/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
-/
import Mathlib.Data.Set.Intervals.Pi
import Mathlib.Data.Set.Pointwise.Interval
import Mathlib.Order.Filter.Interval
import Mathlib.Tactic.TFAE
import Mathlib.Topology.Support
import Mathlib.Topology.Algebra.Order.LeftRight

#align_import topology.order.basic from "leanprover-community/mathlib"@"3efd324a3a31eaa40c9d5bfc669c4fafee5f9423"

/-!
# Theory of topology on ordered spaces

## Main definitions

The order topology on an ordered space is the topology generated by all open intervals (or
equivalently by those of the form `(-∞, a)` and `(b, +∞)`). We define it as `Preorder.topology α`.
However, we do *not* register it as an instance (as many existing ordered types already have
topologies, which would be equal but not definitionally equal to `Preorder.topology α`). Instead,
we introduce a class `OrderTopology α` (which is a `Prop`, also known as a mixin) saying that on
the type `α` having already a topological space structure and a preorder structure, the topological
structure is equal to the order topology.

We also introduce another (mixin) class `OrderClosedTopology α` saying that the set of points
`(x, y)` with `x ≤ y` is closed in the product space. This is automatically satisfied on a linear
order with the order topology.

We prove many basic properties of such topologies.

## Main statements

This file contains the proofs of the following facts. For exact requirements
(`OrderClosedTopology` vs `OrderTopology`, `Preorder` vs `PartialOrder` vs `LinearOrder` etc)
see their statements.

### Open / closed sets

* `isOpen_lt` : if `f` and `g` are continuous functions, then `{x | f x < g x}` is open;
* `isOpen_Iio`, `isOpen_Ioi`, `isOpen_Ioo` : open intervals are open;
* `isClosed_le` : if `f` and `g` are continuous functions, then `{x | f x ≤ g x}` is closed;
* `isClosed_Iic`, `isClosed_Ici`, `isClosed_Icc` : closed intervals are closed;
* `frontier_le_subset_eq`, `frontier_lt_subset_eq` : frontiers of both `{x | f x ≤ g x}`
  and `{x | f x < g x}` are included by `{x | f x = g x}`;
* `exists_Ioc_subset_of_mem_nhds`, `exists_Ico_subset_of_mem_nhds` : if `x < y`, then any
  neighborhood of `x` includes an interval `[x, z)` for some `z ∈ (x, y]`, and any neighborhood
  of `y` includes an interval `(z, y]` for some `z ∈ [x, y)`.

### Convergence and inequalities

* `le_of_tendsto_of_tendsto` : if `f` converges to `a`, `g` converges to `b`, and eventually
  `f x ≤ g x`, then `a ≤ b`
* `le_of_tendsto`, `ge_of_tendsto` : if `f` converges to `a` and eventually `f x ≤ b`
  (resp., `b ≤ f x`), then `a ≤ b` (resp., `b ≤ a`); we also provide primed versions
  that assume the inequalities to hold for all `x`.

### Min, max, `sSup` and `sInf`

* `Continuous.min`, `Continuous.max`: pointwise `min`/`max` of two continuous functions is
  continuous.
* `Tendsto.min`, `Tendsto.max` : if `f` tends to `a` and `g` tends to `b`, then their pointwise
  `min`/`max` tend to `min a b` and `max a b`, respectively.
* `tendsto_of_tendsto_of_tendsto_of_le_of_le` : theorem known as squeeze theorem,
  sandwich theorem, theorem of Carabinieri, and two policemen (and a drunk) theorem; if `g` and `h`
  both converge to `a`, and eventually `g x ≤ f x ≤ h x`, then `f` converges to `a`.

## Implementation notes

We do _not_ register the order topology as an instance on a preorder (or even on a linear order).
Indeed, on many such spaces, a topology has already been constructed in a different way (think
of the discrete spaces `ℕ` or `ℤ`, or `ℝ` that could inherit a topology as the completion of `ℚ`),
and is in general not defeq to the one generated by the intervals. We make it available as a
definition `Preorder.topology α` though, that can be registered as an instance when necessary, or
for specific types.
-/


open Set Filter TopologicalSpace Topology Function

open OrderDual (toDual ofDual)

universe u v w

variable {α : Type u} {β : Type v} {γ : Type w}

/-- If `α` is a topological space and a preorder, `ClosedIicTopology α` means that `Iic a` is
closed for all `a : α`. -/
class ClosedIicTopology (α : Type*) [TopologicalSpace α] [Preorder α] : Prop where
  /-- For any `a`, the set `{b | b ≤ a}` is closed. -/
  isClosed_le' (a : α) : IsClosed { b : α | b ≤ a }

export ClosedIicTopology (isClosed_le')
#align is_closed_le' ClosedIicTopology.isClosed_le'

/-- If `α` is a topological space and a preorder, `ClosedIciTopology α` means that `Ici a` is
closed for all `a : α`. -/
class ClosedIciTopology (α : Type*) [TopologicalSpace α] [Preorder α] : Prop where
  /-- For any `a`, the set `{b | a ≤ b}` is closed. -/
  isClosed_ge' (a : α) : IsClosed { b : α | a ≤ b }

export ClosedIciTopology (isClosed_ge')
#align is_closed_ge' ClosedIciTopology.isClosed_ge'

/-- A topology on a set which is both a topological space and a preorder is _order-closed_ if the
set of points `(x, y)` with `x ≤ y` is closed in the product space. We introduce this as a mixin.
This property is satisfied for the order topology on a linear order, but it can be satisfied more
generally, and suffices to derive many interesting properties relating order and topology. -/
class OrderClosedTopology (α : Type*) [TopologicalSpace α] [Preorder α] : Prop where
  /-- The set `{ (x, y) | x ≤ y }` is a closed set. -/
  isClosed_le' : IsClosed { p : α × α | p.1 ≤ p.2 }
#align order_closed_topology OrderClosedTopology

instance [TopologicalSpace α] [h : FirstCountableTopology α] : FirstCountableTopology αᵒᵈ := h
instance [TopologicalSpace α] [h : SecondCountableTopology α] : SecondCountableTopology αᵒᵈ := h

theorem Dense.orderDual [TopologicalSpace α] {s : Set α} (hs : Dense s) :
    Dense (OrderDual.ofDual ⁻¹' s) :=
  hs
#align dense.order_dual Dense.orderDual

section ClosedIicTopology

variable [TopologicalSpace α] [Preorder α] [t : ClosedIicTopology α]

instance : ClosedIciTopology αᵒᵈ where
  isClosed_ge' a := isClosed_le' (α := α) a

theorem isClosed_Iic {a : α} : IsClosed (Iic a) :=
  isClosed_le' a
#align is_closed_Iic isClosed_Iic

@[simp]
theorem closure_Iic (a : α) : closure (Iic a) = Iic a :=
  isClosed_Iic.closure_eq
#align closure_Iic closure_Iic

theorem le_of_tendsto {f : β → α} {a b : α} {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a))
    (h : ∀ᶠ c in x, f c ≤ b) : a ≤ b :=
  (isClosed_le' b).mem_of_tendsto lim h
#align le_of_tendsto le_of_tendsto

theorem le_of_tendsto' {f : β → α} {a b : α} {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a))
    (h : ∀ c, f c ≤ b) : a ≤ b :=
  le_of_tendsto lim (eventually_of_forall h)
#align le_of_tendsto' le_of_tendsto'

end ClosedIicTopology

section ClosedIciTopology

variable [TopologicalSpace α] [Preorder α] [t : ClosedIciTopology α]

instance : ClosedIicTopology αᵒᵈ where
  isClosed_le' a := isClosed_ge' (α := α) a

theorem isClosed_Ici {a : α} : IsClosed (Ici a) :=
  isClosed_ge' a
#align is_closed_Ici isClosed_Ici

@[simp]
theorem closure_Ici (a : α) : closure (Ici a) = Ici a :=
  isClosed_Ici.closure_eq
#align closure_Ici closure_Ici

theorem ge_of_tendsto {f : β → α} {a b : α} {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a))
    (h : ∀ᶠ c in x, b ≤ f c) : b ≤ a :=
  (isClosed_ge' b).mem_of_tendsto lim h
#align ge_of_tendsto ge_of_tendsto

theorem ge_of_tendsto' {f : β → α} {a b : α} {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a))
    (h : ∀ c, b ≤ f c) : b ≤ a :=
  ge_of_tendsto lim (eventually_of_forall h)
#align ge_of_tendsto' ge_of_tendsto'

end ClosedIciTopology

section OrderClosedTopology

section Preorder

variable [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α]

namespace Subtype

-- todo: add `OrderEmbedding.orderClosedTopology`
instance {p : α → Prop} : OrderClosedTopology (Subtype p) :=
  have this : Continuous fun p : Subtype p × Subtype p => ((p.fst : α), (p.snd : α)) :=
    continuous_subtype_val.prod_map continuous_subtype_val
  OrderClosedTopology.mk (t.isClosed_le'.preimage this)

end Subtype

theorem isClosed_le_prod : IsClosed { p : α × α | p.1 ≤ p.2 } :=
  t.isClosed_le'
#align is_closed_le_prod isClosed_le_prod

theorem isClosed_le [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) :
    IsClosed { b | f b ≤ g b } :=
  continuous_iff_isClosed.mp (hf.prod_mk hg) _ isClosed_le_prod
#align is_closed_le isClosed_le

instance : ClosedIicTopology α where
  isClosed_le' _ := isClosed_le continuous_id continuous_const

instance : ClosedIciTopology α where
  isClosed_ge' _ := isClosed_le continuous_const continuous_id

instance : OrderClosedTopology αᵒᵈ :=
  ⟨(OrderClosedTopology.isClosed_le' (α := α)).preimage continuous_swap⟩

theorem isClosed_Icc {a b : α} : IsClosed (Icc a b) :=
  IsClosed.inter isClosed_Ici isClosed_Iic
#align is_closed_Icc isClosed_Icc

@[simp]
theorem closure_Icc (a b : α) : closure (Icc a b) = Icc a b :=
  isClosed_Icc.closure_eq
#align closure_Icc closure_Icc

theorem le_of_tendsto_of_tendsto {f g : β → α} {b : Filter β} {a₁ a₂ : α} [NeBot b]
    (hf : Tendsto f b (𝓝 a₁)) (hg : Tendsto g b (𝓝 a₂)) (h : f ≤ᶠ[b] g) : a₁ ≤ a₂ :=
  have : Tendsto (fun b => (f b, g b)) b (𝓝 (a₁, a₂)) := hf.prod_mk_nhds hg
  show (a₁, a₂) ∈ { p : α × α | p.1 ≤ p.2 } from t.isClosed_le'.mem_of_tendsto this h
#align le_of_tendsto_of_tendsto le_of_tendsto_of_tendsto

alias tendsto_le_of_eventuallyLE := le_of_tendsto_of_tendsto
#align tendsto_le_of_eventually_le tendsto_le_of_eventuallyLE

theorem le_of_tendsto_of_tendsto' {f g : β → α} {b : Filter β} {a₁ a₂ : α} [NeBot b]
    (hf : Tendsto f b (𝓝 a₁)) (hg : Tendsto g b (𝓝 a₂)) (h : ∀ x, f x ≤ g x) : a₁ ≤ a₂ :=
  le_of_tendsto_of_tendsto hf hg (eventually_of_forall h)
#align le_of_tendsto_of_tendsto' le_of_tendsto_of_tendsto'

@[simp]
theorem closure_le_eq [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) :
    closure { b | f b ≤ g b } = { b | f b ≤ g b } :=
  (isClosed_le hf hg).closure_eq
#align closure_le_eq closure_le_eq

theorem closure_lt_subset_le [TopologicalSpace β] {f g : β → α} (hf : Continuous f)
    (hg : Continuous g) : closure { b | f b < g b } ⊆ { b | f b ≤ g b } :=
  (closure_minimal fun _ => le_of_lt) <| isClosed_le hf hg
#align closure_lt_subset_le closure_lt_subset_le

theorem ContinuousWithinAt.closure_le [TopologicalSpace β] {f g : β → α} {s : Set β} {x : β}
    (hx : x ∈ closure s) (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x)
    (h : ∀ y ∈ s, f y ≤ g y) : f x ≤ g x :=
  show (f x, g x) ∈ { p : α × α | p.1 ≤ p.2 } from
    OrderClosedTopology.isClosed_le'.closure_subset ((hf.prod hg).mem_closure hx h)
#align continuous_within_at.closure_le ContinuousWithinAt.closure_le

/-- If `s` is a closed set and two functions `f` and `g` are continuous on `s`,
then the set `{x ∈ s | f x ≤ g x}` is a closed set. -/
theorem IsClosed.isClosed_le [TopologicalSpace β] {f g : β → α} {s : Set β} (hs : IsClosed s)
    (hf : ContinuousOn f s) (hg : ContinuousOn g s) : IsClosed ({ x ∈ s | f x ≤ g x }) :=
  (hf.prod hg).preimage_closed_of_closed hs OrderClosedTopology.isClosed_le'
#align is_closed.is_closed_le IsClosed.isClosed_le

theorem le_on_closure [TopologicalSpace β] {f g : β → α} {s : Set β} (h : ∀ x ∈ s, f x ≤ g x)
    (hf : ContinuousOn f (closure s)) (hg : ContinuousOn g (closure s)) ⦃x⦄ (hx : x ∈ closure s) :
    f x ≤ g x :=
  have : s ⊆ { y ∈ closure s | f y ≤ g y } := fun y hy => ⟨subset_closure hy, h y hy⟩
  (closure_minimal this (isClosed_closure.isClosed_le hf hg) hx).2
#align le_on_closure le_on_closure

theorem IsClosed.epigraph [TopologicalSpace β] {f : β → α} {s : Set β} (hs : IsClosed s)
    (hf : ContinuousOn f s) : IsClosed { p : β × α | p.1 ∈ s ∧ f p.1 ≤ p.2 } :=
  (hs.preimage continuous_fst).isClosed_le (hf.comp continuousOn_fst Subset.rfl) continuousOn_snd
#align is_closed.epigraph IsClosed.epigraph

theorem IsClosed.hypograph [TopologicalSpace β] {f : β → α} {s : Set β} (hs : IsClosed s)
    (hf : ContinuousOn f s) : IsClosed { p : β × α | p.1 ∈ s ∧ p.2 ≤ f p.1 } :=
  (hs.preimage continuous_fst).isClosed_le continuousOn_snd (hf.comp continuousOn_fst Subset.rfl)
#align is_closed.hypograph IsClosed.hypograph

-- Porting note: todo: move these lemmas to `Topology.Algebra.Order.LeftRight`
theorem nhdsWithin_Ici_neBot {a b : α} (H₂ : a ≤ b) : NeBot (𝓝[Ici a] b) :=
  nhdsWithin_neBot_of_mem H₂
#align nhds_within_Ici_ne_bot nhdsWithin_Ici_neBot

@[instance]
theorem nhdsWithin_Ici_self_neBot (a : α) : NeBot (𝓝[≥] a) :=
  nhdsWithin_Ici_neBot (le_refl a)
#align nhds_within_Ici_self_ne_bot nhdsWithin_Ici_self_neBot

theorem nhdsWithin_Iic_neBot {a b : α} (H : a ≤ b) : NeBot (𝓝[Iic b] a) :=
  nhdsWithin_neBot_of_mem H
#align nhds_within_Iic_ne_bot nhdsWithin_Iic_neBot

@[instance]
theorem nhdsWithin_Iic_self_neBot (a : α) : NeBot (𝓝[≤] a) :=
  nhdsWithin_Iic_neBot (le_refl a)
#align nhds_within_Iic_self_ne_bot nhdsWithin_Iic_self_neBot

end Preorder

section PartialOrder

variable [TopologicalSpace α] [PartialOrder α] [t : OrderClosedTopology α]

-- see Note [lower instance priority]
instance (priority := 90) OrderClosedTopology.to_t2Space : T2Space α :=
  t2_iff_isClosed_diagonal.2 <| by
    simpa only [diagonal, le_antisymm_iff] using
      t.isClosed_le'.inter (isClosed_le continuous_snd continuous_fst)
#align order_closed_topology.to_t2_space OrderClosedTopology.to_t2Space

end PartialOrder

section LinearOrder

variable [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α]

theorem isOpen_lt [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) :
    IsOpen { b | f b < g b } := by
  simpa only [lt_iff_not_le] using (isClosed_le hg hf).isOpen_compl
#align is_open_lt isOpen_lt

theorem isOpen_lt_prod : IsOpen { p : α × α | p.1 < p.2 } :=
  isOpen_lt continuous_fst continuous_snd
#align is_open_lt_prod isOpen_lt_prod

variable {a b : α}

theorem isOpen_Iio : IsOpen (Iio a) :=
  isOpen_lt continuous_id continuous_const
#align is_open_Iio isOpen_Iio

theorem isOpen_Ioi : IsOpen (Ioi a) :=
  isOpen_lt continuous_const continuous_id
#align is_open_Ioi isOpen_Ioi

theorem isOpen_Ioo : IsOpen (Ioo a b) :=
  IsOpen.inter isOpen_Ioi isOpen_Iio
#align is_open_Ioo isOpen_Ioo

@[simp]
theorem interior_Ioi : interior (Ioi a) = Ioi a :=
  isOpen_Ioi.interior_eq
#align interior_Ioi interior_Ioi

@[simp]
theorem interior_Iio : interior (Iio a) = Iio a :=
  isOpen_Iio.interior_eq
#align interior_Iio interior_Iio

@[simp]
theorem interior_Ioo : interior (Ioo a b) = Ioo a b :=
  isOpen_Ioo.interior_eq
#align interior_Ioo interior_Ioo

theorem Ioo_subset_closure_interior : Ioo a b ⊆ closure (interior (Ioo a b)) := by
  simp only [interior_Ioo, subset_closure]
#align Ioo_subset_closure_interior Ioo_subset_closure_interior

theorem Iio_mem_nhds {a b : α} (h : a < b) : Iio b ∈ 𝓝 a :=
  IsOpen.mem_nhds isOpen_Iio h
#align Iio_mem_nhds Iio_mem_nhds

theorem Ioi_mem_nhds {a b : α} (h : a < b) : Ioi a ∈ 𝓝 b :=
  IsOpen.mem_nhds isOpen_Ioi h
#align Ioi_mem_nhds Ioi_mem_nhds

theorem Iic_mem_nhds {a b : α} (h : a < b) : Iic b ∈ 𝓝 a :=
  mem_of_superset (Iio_mem_nhds h) Iio_subset_Iic_self
#align Iic_mem_nhds Iic_mem_nhds

theorem Ici_mem_nhds {a b : α} (h : a < b) : Ici a ∈ 𝓝 b :=
  mem_of_superset (Ioi_mem_nhds h) Ioi_subset_Ici_self
#align Ici_mem_nhds Ici_mem_nhds

theorem Ioo_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ioo a b ∈ 𝓝 x :=
  IsOpen.mem_nhds isOpen_Ioo ⟨ha, hb⟩
#align Ioo_mem_nhds Ioo_mem_nhds

theorem Ioc_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ioc a b ∈ 𝓝 x :=
  mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Ioc_self
#align Ioc_mem_nhds Ioc_mem_nhds

theorem Ico_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ico a b ∈ 𝓝 x :=
  mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Ico_self
#align Ico_mem_nhds Ico_mem_nhds

theorem Icc_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Icc a b ∈ 𝓝 x :=
  mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Icc_self
#align Icc_mem_nhds Icc_mem_nhds

theorem eventually_lt_of_tendsto_lt {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u)
    (h : Filter.Tendsto f l (𝓝 v)) : ∀ᶠ a in l, f a < u :=
  tendsto_nhds.1 h (· < u) isOpen_Iio hv
#align eventually_lt_of_tendsto_lt eventually_lt_of_tendsto_lt

theorem eventually_gt_of_tendsto_gt {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v)
    (h : Filter.Tendsto f l (𝓝 v)) : ∀ᶠ a in l, u < f a :=
  tendsto_nhds.1 h (· > u) isOpen_Ioi hv
#align eventually_gt_of_tendsto_gt eventually_gt_of_tendsto_gt

theorem eventually_le_of_tendsto_lt {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u)
    (h : Tendsto f l (𝓝 v)) : ∀ᶠ a in l, f a ≤ u :=
  (eventually_lt_of_tendsto_lt hv h).mono fun _ => le_of_lt
#align eventually_le_of_tendsto_lt eventually_le_of_tendsto_lt

theorem eventually_ge_of_tendsto_gt {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v)
    (h : Tendsto f l (𝓝 v)) : ∀ᶠ a in l, u ≤ f a :=
  (eventually_gt_of_tendsto_gt hv h).mono fun _ => le_of_lt
#align eventually_ge_of_tendsto_gt eventually_ge_of_tendsto_gt

variable [TopologicalSpace γ]

/-!
### Neighborhoods to the left and to the right on an `OrderClosedTopology`

Limits to the left and to the right of real functions are defined in terms of neighborhoods to
the left and to the right, either open or closed, i.e., members of `𝓝[>] a` and
`𝓝[≥] a` on the right, and similarly on the left. Here we simply prove that all
right-neighborhoods of a point are equal, and we'll prove later other useful characterizations which
require the stronger hypothesis `OrderTopology α` -/


/-!
#### Right neighborhoods, point excluded
-/

theorem Ioo_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Ioo a c ∈ 𝓝[>] b :=
  mem_nhdsWithin.2
    ⟨Iio c, isOpen_Iio, H.2, by rw [inter_comm, Ioi_inter_Iio]; exact Ioo_subset_Ioo_left H.1⟩
#align Ioo_mem_nhds_within_Ioi Ioo_mem_nhdsWithin_Ioi

-- porting note: new lemma; todo: swap `'`?
theorem Ioo_mem_nhdsWithin_Ioi' {a b : α} (H : a < b) : Ioo a b ∈ 𝓝[>] a :=
  Ioo_mem_nhdsWithin_Ioi ⟨le_rfl, H⟩

theorem Covby.nhdsWithin_Ioi {a b : α} (h : a ⋖ b) : 𝓝[>] a = ⊥ :=
  empty_mem_iff_bot.mp <| h.Ioo_eq ▸ Ioo_mem_nhdsWithin_Ioi' h.1

theorem Ioc_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Ioc a c ∈ 𝓝[>] b :=
  mem_of_superset (Ioo_mem_nhdsWithin_Ioi H) Ioo_subset_Ioc_self
#align Ioc_mem_nhds_within_Ioi Ioc_mem_nhdsWithin_Ioi

-- porting note: new lemma; todo: swap `'`?
theorem Ioc_mem_nhdsWithin_Ioi' {a b : α} (H : a < b) : Ioc a b ∈ 𝓝[>] a :=
  Ioc_mem_nhdsWithin_Ioi ⟨le_rfl, H⟩

theorem Ico_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Ico a c ∈ 𝓝[>] b :=
  mem_of_superset (Ioo_mem_nhdsWithin_Ioi H) Ioo_subset_Ico_self
#align Ico_mem_nhds_within_Ioi Ico_mem_nhdsWithin_Ioi

-- porting note: new lemma; todo: swap `'`?
theorem Ico_mem_nhdsWithin_Ioi' {a b : α} (H : a < b) : Ico a b ∈ 𝓝[>] a :=
  Ico_mem_nhdsWithin_Ioi ⟨le_rfl, H⟩

theorem Icc_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Icc a c ∈ 𝓝[>] b :=
  mem_of_superset (Ioo_mem_nhdsWithin_Ioi H) Ioo_subset_Icc_self
#align Icc_mem_nhds_within_Ioi Icc_mem_nhdsWithin_Ioi

-- porting note: new lemma; todo: swap `'`?
theorem Icc_mem_nhdsWithin_Ioi' {a b : α} (H : a < b) : Icc a b ∈ 𝓝[>] a :=
  Icc_mem_nhdsWithin_Ioi ⟨le_rfl, H⟩

@[simp]
theorem nhdsWithin_Ioc_eq_nhdsWithin_Ioi {a b : α} (h : a < b) : 𝓝[Ioc a b] a = 𝓝[>] a :=
  nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iic_mem_nhds h
#align nhds_within_Ioc_eq_nhds_within_Ioi nhdsWithin_Ioc_eq_nhdsWithin_Ioi

@[simp]
theorem nhdsWithin_Ioo_eq_nhdsWithin_Ioi {a b : α} (h : a < b) : 𝓝[Ioo a b] a = 𝓝[>] a :=
  nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iio_mem_nhds h
#align nhds_within_Ioo_eq_nhds_within_Ioi nhdsWithin_Ioo_eq_nhdsWithin_Ioi

@[simp]
theorem continuousWithinAt_Ioc_iff_Ioi [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) :
    ContinuousWithinAt f (Ioc a b) a ↔ ContinuousWithinAt f (Ioi a) a := by
  simp only [ContinuousWithinAt, nhdsWithin_Ioc_eq_nhdsWithin_Ioi h]
#align continuous_within_at_Ioc_iff_Ioi continuousWithinAt_Ioc_iff_Ioi

@[simp]
theorem continuousWithinAt_Ioo_iff_Ioi [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) :
    ContinuousWithinAt f (Ioo a b) a ↔ ContinuousWithinAt f (Ioi a) a := by
  simp only [ContinuousWithinAt, nhdsWithin_Ioo_eq_nhdsWithin_Ioi h]
#align continuous_within_at_Ioo_iff_Ioi continuousWithinAt_Ioo_iff_Ioi

/-!
#### Left neighborhoods, point excluded
-/

theorem Ioo_mem_nhdsWithin_Iio {a b c : α} (H : b ∈ Ioc a c) : Ioo a c ∈ 𝓝[<] b := by
  simpa only [dual_Ioo] using
    Ioo_mem_nhdsWithin_Ioi (show toDual b ∈ Ico (toDual c) (toDual a) from H.symm)
#align Ioo_mem_nhds_within_Iio Ioo_mem_nhdsWithin_Iio

-- porting note: new lemma; todo: swap `'`?
theorem Ioo_mem_nhdsWithin_Iio' {a b : α} (H : a < b) : Ioo a b ∈ 𝓝[<] b :=
  Ioo_mem_nhdsWithin_Iio ⟨H, le_rfl⟩

theorem Covby.nhdsWithin_Iio {a b : α} (h : a ⋖ b) : 𝓝[<] b = ⊥ :=
  empty_mem_iff_bot.mp <| h.Ioo_eq ▸ Ioo_mem_nhdsWithin_Iio' h.1

theorem Ico_mem_nhdsWithin_Iio {a b c : α} (H : b ∈ Ioc a c) : Ico a c ∈ 𝓝[<] b :=
  mem_of_superset (Ioo_mem_nhdsWithin_Iio H) Ioo_subset_Ico_self
#align Ico_mem_nhds_within_Iio Ico_mem_nhdsWithin_Iio

-- porting note: new lemma; todo: swap `'`?
theorem Ico_mem_nhdsWithin_Iio' {a b : α} (H : a < b) : Ico a b ∈ 𝓝[<] b :=
  Ico_mem_nhdsWithin_Iio ⟨H, le_rfl⟩

theorem Ioc_mem_nhdsWithin_Iio {a b c : α} (H : b ∈ Ioc a c) : Ioc a c ∈ 𝓝[<] b :=
  mem_of_superset (Ioo_mem_nhdsWithin_Iio H) Ioo_subset_Ioc_self
#align Ioc_mem_nhds_within_Iio Ioc_mem_nhdsWithin_Iio

-- porting note: new lemma; todo: swap `'`?
theorem Ioc_mem_nhdsWithin_Iio' {a b : α} (H : a < b) : Ioc a b ∈ 𝓝[<] b :=
  Ioc_mem_nhdsWithin_Iio ⟨H, le_rfl⟩

theorem Icc_mem_nhdsWithin_Iio {a b c : α} (H : b ∈ Ioc a c) : Icc a c ∈ 𝓝[<] b :=
  mem_of_superset (Ioo_mem_nhdsWithin_Iio H) Ioo_subset_Icc_self
#align Icc_mem_nhds_within_Iio Icc_mem_nhdsWithin_Iio

theorem Icc_mem_nhdsWithin_Iio' {a b : α} (H : a < b) : Icc a b ∈ 𝓝[<] b :=
  Icc_mem_nhdsWithin_Iio ⟨H, le_rfl⟩

@[simp]
theorem nhdsWithin_Ico_eq_nhdsWithin_Iio {a b : α} (h : a < b) : 𝓝[Ico a b] b = 𝓝[<] b := by
  simpa only [dual_Ioc] using nhdsWithin_Ioc_eq_nhdsWithin_Ioi h.dual
#align nhds_within_Ico_eq_nhds_within_Iio nhdsWithin_Ico_eq_nhdsWithin_Iio

@[simp]
theorem nhdsWithin_Ioo_eq_nhdsWithin_Iio {a b : α} (h : a < b) : 𝓝[Ioo a b] b = 𝓝[<] b := by
  simpa only [dual_Ioo] using nhdsWithin_Ioo_eq_nhdsWithin_Ioi h.dual
#align nhds_within_Ioo_eq_nhds_within_Iio nhdsWithin_Ioo_eq_nhdsWithin_Iio

@[simp]
theorem continuousWithinAt_Ico_iff_Iio {a b : α} {f : α → γ} (h : a < b) :
    ContinuousWithinAt f (Ico a b) b ↔ ContinuousWithinAt f (Iio b) b := by
  simp only [ContinuousWithinAt, nhdsWithin_Ico_eq_nhdsWithin_Iio h]
#align continuous_within_at_Ico_iff_Iio continuousWithinAt_Ico_iff_Iio

@[simp]
theorem continuousWithinAt_Ioo_iff_Iio {a b : α} {f : α → γ} (h : a < b) :
    ContinuousWithinAt f (Ioo a b) b ↔ ContinuousWithinAt f (Iio b) b := by
  simp only [ContinuousWithinAt, nhdsWithin_Ioo_eq_nhdsWithin_Iio h]
#align continuous_within_at_Ioo_iff_Iio continuousWithinAt_Ioo_iff_Iio

/-!
#### Right neighborhoods, point included
-/

theorem Ioo_mem_nhdsWithin_Ici {a b c : α} (H : b ∈ Ioo a c) : Ioo a c ∈ 𝓝[≥] b :=
  mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds isOpen_Ioo H
#align Ioo_mem_nhds_within_Ici Ioo_mem_nhdsWithin_Ici

theorem Ioc_mem_nhdsWithin_Ici {a b c : α} (H : b ∈ Ioo a c) : Ioc a c ∈ 𝓝[≥] b :=
  mem_of_superset (Ioo_mem_nhdsWithin_Ici H) Ioo_subset_Ioc_self
#align Ioc_mem_nhds_within_Ici Ioc_mem_nhdsWithin_Ici

theorem Ico_mem_nhdsWithin_Ici {a b c : α} (H : b ∈ Ico a c) : Ico a c ∈ 𝓝[≥] b :=
  mem_nhdsWithin.2
    ⟨Iio c, isOpen_Iio, H.2, by simp only [inter_comm, Ici_inter_Iio, Ico_subset_Ico_left H.1]⟩
#align Ico_mem_nhds_within_Ici Ico_mem_nhdsWithin_Ici

theorem Ico_mem_nhdsWithin_Ici' {a b : α} (H : a < b) : Ico a b ∈ 𝓝[≥] a :=
  Ico_mem_nhdsWithin_Ici ⟨le_rfl, H⟩

theorem Icc_mem_nhdsWithin_Ici {a b c : α} (H : b ∈ Ico a c) : Icc a c ∈ 𝓝[≥] b :=
  mem_of_superset (Ico_mem_nhdsWithin_Ici H) Ico_subset_Icc_self
#align Icc_mem_nhds_within_Ici Icc_mem_nhdsWithin_Ici

theorem Icc_mem_nhdsWithin_Ici' {a b : α} (H : a < b) : Icc a b ∈ 𝓝[≥] a :=
  Icc_mem_nhdsWithin_Ici ⟨le_rfl, H⟩

@[simp]
theorem nhdsWithin_Icc_eq_nhdsWithin_Ici {a b : α} (h : a < b) : 𝓝[Icc a b] a = 𝓝[≥] a :=
  nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iic_mem_nhds h
#align nhds_within_Icc_eq_nhds_within_Ici nhdsWithin_Icc_eq_nhdsWithin_Ici

@[simp]
theorem nhdsWithin_Ico_eq_nhdsWithin_Ici {a b : α} (h : a < b) : 𝓝[Ico a b] a = 𝓝[≥] a :=
  nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iio_mem_nhds h
#align nhds_within_Ico_eq_nhds_within_Ici nhdsWithin_Ico_eq_nhdsWithin_Ici

@[simp]
theorem continuousWithinAt_Icc_iff_Ici [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) :
    ContinuousWithinAt f (Icc a b) a ↔ ContinuousWithinAt f (Ici a) a := by
  simp only [ContinuousWithinAt, nhdsWithin_Icc_eq_nhdsWithin_Ici h]
#align continuous_within_at_Icc_iff_Ici continuousWithinAt_Icc_iff_Ici

@[simp]
theorem continuousWithinAt_Ico_iff_Ici [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) :
    ContinuousWithinAt f (Ico a b) a ↔ ContinuousWithinAt f (Ici a) a := by
  simp only [ContinuousWithinAt, nhdsWithin_Ico_eq_nhdsWithin_Ici h]
#align continuous_within_at_Ico_iff_Ici continuousWithinAt_Ico_iff_Ici

/-!
#### Left neighborhoods, point included
-/


theorem Ioo_mem_nhdsWithin_Iic {a b c : α} (H : b ∈ Ioo a c) : Ioo a c ∈ 𝓝[≤] b :=
  mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds isOpen_Ioo H
#align Ioo_mem_nhds_within_Iic Ioo_mem_nhdsWithin_Iic

theorem Ico_mem_nhdsWithin_Iic {a b c : α} (H : b ∈ Ioo a c) : Ico a c ∈ 𝓝[≤] b :=
  mem_of_superset (Ioo_mem_nhdsWithin_Iic H) Ioo_subset_Ico_self
#align Ico_mem_nhds_within_Iic Ico_mem_nhdsWithin_Iic

theorem Ioc_mem_nhdsWithin_Iic {a b c : α} (H : b ∈ Ioc a c) : Ioc a c ∈ 𝓝[≤] b := by
  simpa only [dual_Ico] using
    Ico_mem_nhdsWithin_Ici (show toDual b ∈ Ico (toDual c) (toDual a) from H.symm)
#align Ioc_mem_nhds_within_Iic Ioc_mem_nhdsWithin_Iic

theorem Ioc_mem_nhdsWithin_Iic' {a b : α} (H : a < b) : Ioc a b ∈ 𝓝[≤] b :=
  Ioc_mem_nhdsWithin_Iic ⟨H, le_rfl⟩

theorem Icc_mem_nhdsWithin_Iic {a b c : α} (H : b ∈ Ioc a c) : Icc a c ∈ 𝓝[≤] b :=
  mem_of_superset (Ioc_mem_nhdsWithin_Iic H) Ioc_subset_Icc_self
#align Icc_mem_nhds_within_Iic Icc_mem_nhdsWithin_Iic

theorem Icc_mem_nhdsWithin_Iic' {a b : α} (H : a < b) : Icc a b ∈ 𝓝[≤] b :=
  Icc_mem_nhdsWithin_Iic ⟨H, le_rfl⟩

@[simp]
theorem nhdsWithin_Icc_eq_nhdsWithin_Iic {a b : α} (h : a < b) : 𝓝[Icc a b] b = 𝓝[≤] b := by
  simpa only [dual_Icc] using nhdsWithin_Icc_eq_nhdsWithin_Ici h.dual
#align nhds_within_Icc_eq_nhds_within_Iic nhdsWithin_Icc_eq_nhdsWithin_Iic

@[simp]
theorem nhdsWithin_Ioc_eq_nhdsWithin_Iic {a b : α} (h : a < b) : 𝓝[Ioc a b] b = 𝓝[≤] b := by
  simpa only [dual_Ico] using nhdsWithin_Ico_eq_nhdsWithin_Ici h.dual
#align nhds_within_Ioc_eq_nhds_within_Iic nhdsWithin_Ioc_eq_nhdsWithin_Iic

@[simp]
theorem continuousWithinAt_Icc_iff_Iic [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) :
    ContinuousWithinAt f (Icc a b) b ↔ ContinuousWithinAt f (Iic b) b := by
  simp only [ContinuousWithinAt, nhdsWithin_Icc_eq_nhdsWithin_Iic h]
#align continuous_within_at_Icc_iff_Iic continuousWithinAt_Icc_iff_Iic

@[simp]
theorem continuousWithinAt_Ioc_iff_Iic [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) :
    ContinuousWithinAt f (Ioc a b) b ↔ ContinuousWithinAt f (Iic b) b := by
  simp only [ContinuousWithinAt, nhdsWithin_Ioc_eq_nhdsWithin_Iic h]
#align continuous_within_at_Ioc_iff_Iic continuousWithinAt_Ioc_iff_Iic

end LinearOrder

section LinearOrder

variable [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α}

section

variable [TopologicalSpace β]

theorem lt_subset_interior_le (hf : Continuous f) (hg : Continuous g) :
    { b | f b < g b } ⊆ interior { b | f b ≤ g b } :=
  (interior_maximal fun _ => le_of_lt) <| isOpen_lt hf hg
#align lt_subset_interior_le lt_subset_interior_le

theorem frontier_le_subset_eq (hf : Continuous f) (hg : Continuous g) :
    frontier { b | f b ≤ g b } ⊆ { b | f b = g b } := by
  rw [frontier_eq_closure_inter_closure, closure_le_eq hf hg]
  rintro b ⟨hb₁, hb₂⟩
  refine' le_antisymm hb₁ (closure_lt_subset_le hg hf _)
  convert hb₂ using 2; simp only [not_le.symm]; rfl
#align frontier_le_subset_eq frontier_le_subset_eq

theorem frontier_Iic_subset (a : α) : frontier (Iic a) ⊆ {a} :=
  frontier_le_subset_eq (@continuous_id α _) continuous_const
#align frontier_Iic_subset frontier_Iic_subset

theorem frontier_Ici_subset (a : α) : frontier (Ici a) ⊆ {a} :=
  frontier_Iic_subset (α := αᵒᵈ) _
#align frontier_Ici_subset frontier_Ici_subset

theorem frontier_lt_subset_eq (hf : Continuous f) (hg : Continuous g) :
    frontier { b | f b < g b } ⊆ { b | f b = g b } := by
  simpa only [← not_lt, ← compl_setOf, frontier_compl, eq_comm] using frontier_le_subset_eq hg hf
#align frontier_lt_subset_eq frontier_lt_subset_eq

theorem continuous_if_le [TopologicalSpace γ] [∀ x, Decidable (f x ≤ g x)] {f' g' : β → γ}
    (hf : Continuous f) (hg : Continuous g) (hf' : ContinuousOn f' { x | f x ≤ g x })
    (hg' : ContinuousOn g' { x | g x ≤ f x }) (hfg : ∀ x, f x = g x → f' x = g' x) :
    Continuous fun x => if f x ≤ g x then f' x else g' x := by
  refine' continuous_if (fun a ha => hfg _ (frontier_le_subset_eq hf hg ha)) _ (hg'.mono _)
  · rwa [(isClosed_le hf hg).closure_eq]
  · simp only [not_le]
    exact closure_lt_subset_le hg hf
#align continuous_if_le continuous_if_le

theorem Continuous.if_le [TopologicalSpace γ] [∀ x, Decidable (f x ≤ g x)] {f' g' : β → γ}
    (hf' : Continuous f') (hg' : Continuous g') (hf : Continuous f) (hg : Continuous g)
    (hfg : ∀ x, f x = g x → f' x = g' x) : Continuous fun x => if f x ≤ g x then f' x else g' x :=
  continuous_if_le hf hg hf'.continuousOn hg'.continuousOn hfg
#align continuous.if_le Continuous.if_le

theorem Filter.Tendsto.eventually_lt {l : Filter γ} {f g : γ → α} {y z : α} (hf : Tendsto f l (𝓝 y))
    (hg : Tendsto g l (𝓝 z)) (hyz : y < z) : ∀ᶠ x in l, f x < g x :=
  let ⟨_a, ha, _b, hb, h⟩ := hyz.exists_disjoint_Iio_Ioi
  (hg.eventually (Ioi_mem_nhds hb)).mp <| (hf.eventually (Iio_mem_nhds ha)).mono fun _ h₁ h₂ =>
    h _ h₁ _ h₂
#align tendsto.eventually_lt Filter.Tendsto.eventually_lt

nonrec theorem ContinuousAt.eventually_lt {x₀ : β} (hf : ContinuousAt f x₀) (hg : ContinuousAt g x₀)
    (hfg : f x₀ < g x₀) : ∀ᶠ x in 𝓝 x₀, f x < g x :=
  hf.eventually_lt hg hfg
#align continuous_at.eventually_lt ContinuousAt.eventually_lt

@[continuity]
protected theorem Continuous.min (hf : Continuous f) (hg : Continuous g) :
    Continuous fun b => min (f b) (g b) := by
  simp only [min_def]
  exact hf.if_le hg hf hg fun x => id
#align continuous.min Continuous.min

@[continuity]
protected theorem Continuous.max (hf : Continuous f) (hg : Continuous g) :
    Continuous fun b => max (f b) (g b) :=
  Continuous.min (α := αᵒᵈ) hf hg
#align continuous.max Continuous.max

end

theorem continuous_min : Continuous fun p : α × α => min p.1 p.2 :=
  continuous_fst.min continuous_snd
#align continuous_min continuous_min

theorem continuous_max : Continuous fun p : α × α => max p.1 p.2 :=
  continuous_fst.max continuous_snd
#align continuous_max continuous_max

protected theorem Filter.Tendsto.max {b : Filter β} {a₁ a₂ : α} (hf : Tendsto f b (𝓝 a₁))
    (hg : Tendsto g b (𝓝 a₂)) : Tendsto (fun b => max (f b) (g b)) b (𝓝 (max a₁ a₂)) :=
  (continuous_max.tendsto (a₁, a₂)).comp (hf.prod_mk_nhds hg)
#align filter.tendsto.max Filter.Tendsto.max

protected theorem Filter.Tendsto.min {b : Filter β} {a₁ a₂ : α} (hf : Tendsto f b (𝓝 a₁))
    (hg : Tendsto g b (𝓝 a₂)) : Tendsto (fun b => min (f b) (g b)) b (𝓝 (min a₁ a₂)) :=
  (continuous_min.tendsto (a₁, a₂)).comp (hf.prod_mk_nhds hg)
#align filter.tendsto.min Filter.Tendsto.min

protected theorem Filter.Tendsto.max_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) :
    Tendsto (fun i => max a (f i)) l (𝓝 a) := by
  convert ((continuous_max.comp (@Continuous.Prod.mk α α _ _ a)).tendsto a).comp h
  simp
#align filter.tendsto.max_right Filter.Tendsto.max_right

protected theorem Filter.Tendsto.max_left {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) :
    Tendsto (fun i => max (f i) a) l (𝓝 a) := by
  simp_rw [max_comm _ a]
  exact h.max_right
#align filter.tendsto.max_left Filter.Tendsto.max_left

theorem Filter.tendsto_nhds_max_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝[>] a)) :
    Tendsto (fun i => max a (f i)) l (𝓝[>] a) := by
  obtain ⟨h₁ : Tendsto f l (𝓝 a), h₂ : ∀ᶠ i in l, f i ∈ Ioi a⟩ := tendsto_nhdsWithin_iff.mp h
  exact tendsto_nhdsWithin_iff.mpr ⟨h₁.max_right, h₂.mono fun i hi => lt_max_of_lt_right hi⟩
#align filter.tendsto_nhds_max_right Filter.tendsto_nhds_max_right

theorem Filter.tendsto_nhds_max_left {l : Filter β} {a : α} (h : Tendsto f l (𝓝[>] a)) :
    Tendsto (fun i => max (f i) a) l (𝓝[>] a) := by
  simp_rw [max_comm _ a]
  exact Filter.tendsto_nhds_max_right h
#align filter.tendsto_nhds_max_left Filter.tendsto_nhds_max_left

theorem Filter.Tendsto.min_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) :
    Tendsto (fun i => min a (f i)) l (𝓝 a) :=
  Filter.Tendsto.max_right (α := αᵒᵈ) h
#align filter.tendsto.min_right Filter.Tendsto.min_right

theorem Filter.Tendsto.min_left {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) :
    Tendsto (fun i => min (f i) a) l (𝓝 a) :=
  Filter.Tendsto.max_left (α := αᵒᵈ) h
#align filter.tendsto.min_left Filter.Tendsto.min_left

theorem Filter.tendsto_nhds_min_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝[<] a)) :
    Tendsto (fun i => min a (f i)) l (𝓝[<] a) :=
  Filter.tendsto_nhds_max_right (α := αᵒᵈ) h
#align filter.tendsto_nhds_min_right Filter.tendsto_nhds_min_right

theorem Filter.tendsto_nhds_min_left {l : Filter β} {a : α} (h : Tendsto f l (𝓝[<] a)) :
    Tendsto (fun i => min (f i) a) l (𝓝[<] a) :=
  Filter.tendsto_nhds_max_left (α := αᵒᵈ) h
#align filter.tendsto_nhds_min_left Filter.tendsto_nhds_min_left

protected theorem Dense.exists_lt [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) :
    ∃ y ∈ s, y < x :=
  hs.exists_mem_open isOpen_Iio (exists_lt x)
#align dense.exists_lt Dense.exists_lt

protected theorem Dense.exists_gt [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) :
    ∃ y ∈ s, x < y :=
  hs.orderDual.exists_lt x
#align dense.exists_gt Dense.exists_gt

protected theorem Dense.exists_le [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) :
    ∃ y ∈ s, y ≤ x :=
  (hs.exists_lt x).imp fun _ h => ⟨h.1, h.2.le⟩
#align dense.exists_le Dense.exists_le

protected theorem Dense.exists_ge [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) :
    ∃ y ∈ s, x ≤ y :=
  hs.orderDual.exists_le x
#align dense.exists_ge Dense.exists_ge

theorem Dense.exists_le' {s : Set α} (hs : Dense s) (hbot : ∀ x, IsBot x → x ∈ s) (x : α) :
    ∃ y ∈ s, y ≤ x := by
  by_cases hx : IsBot x
  · exact ⟨x, hbot x hx, le_rfl⟩
  · simp only [IsBot, not_forall, not_le] at hx
    rcases hs.exists_mem_open isOpen_Iio hx with ⟨y, hys, hy : y < x⟩
    exact ⟨y, hys, hy.le⟩
#align dense.exists_le' Dense.exists_le'

theorem Dense.exists_ge' {s : Set α} (hs : Dense s) (htop : ∀ x, IsTop x → x ∈ s) (x : α) :
    ∃ y ∈ s, x ≤ y :=
  hs.orderDual.exists_le' htop x
#align dense.exists_ge' Dense.exists_ge'

theorem Dense.exists_between [DenselyOrdered α] {s : Set α} (hs : Dense s) {x y : α} (h : x < y) :
    ∃ z ∈ s, z ∈ Ioo x y :=
  hs.exists_mem_open isOpen_Ioo (nonempty_Ioo.2 h)
#align dense.exists_between Dense.exists_between

theorem Dense.Ioi_eq_biUnion [DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) :
    Ioi x = ⋃ y ∈ s ∩ Ioi x, Ioi y := by
  refine Subset.antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun y hy ↦ Ioi_subset_Ioi (le_of_lt hy.2))
  rcases hs.exists_between hz with ⟨y, hys, hxy, hyz⟩
  exact mem_iUnion₂.2 ⟨y, ⟨hys, hxy⟩, hyz⟩

theorem Dense.Iio_eq_biUnion [DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) :
    Iio x = ⋃ y ∈ s ∩ Iio x, Iio y :=
  Dense.Ioi_eq_biUnion (α := αᵒᵈ) hs x

end LinearOrder

end OrderClosedTopology

instance [Preorder α] [TopologicalSpace α] [OrderClosedTopology α] [Preorder β] [TopologicalSpace β]
    [OrderClosedTopology β] : OrderClosedTopology (α × β) :=
  ⟨(isClosed_le continuous_fst.fst continuous_snd.fst).inter
    (isClosed_le continuous_fst.snd continuous_snd.snd)⟩

instance {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)]
    [∀ i, OrderClosedTopology (α i)] : OrderClosedTopology (∀ i, α i) := by
  constructor
  simp only [Pi.le_def, setOf_forall]
  exact isClosed_iInter fun i => isClosed_le (continuous_apply i).fst' (continuous_apply i).snd'

instance Pi.orderClosedTopology' [Preorder β] [TopologicalSpace β] [OrderClosedTopology β] :
    OrderClosedTopology (α → β) :=
  inferInstance
#align pi.order_closed_topology' Pi.orderClosedTopology'

-- porting note: todo: define `Preorder.topology` before `OrderTopology` and reuse the def
/-- The order topology on an ordered type is the topology generated by open intervals. We register
it on a preorder, but it is mostly interesting in linear orders, where it is also order-closed.
We define it as a mixin. If you want to introduce the order topology on a preorder, use
`Preorder.topology`. -/
class OrderTopology (α : Type*) [t : TopologicalSpace α] [Preorder α] : Prop where
  /-- The topology is generated by open intervals `Set.Ioi _` and `Set.Iio _`. -/
  topology_eq_generate_intervals : t = generateFrom { s | ∃ a, s = Ioi a ∨ s = Iio a }
#align order_topology OrderTopology

/-- (Order) topology on a partial order `α` generated by the subbase of open intervals
`(a, ∞) = { x ∣ a < x }, (-∞ , b) = {x ∣ x < b}` for all `a, b` in `α`. We do not register it as an
instance as many ordered sets are already endowed with the same topology, most often in a non-defeq
way though. Register as a local instance when necessary. -/
def Preorder.topology (α : Type*) [Preorder α] : TopologicalSpace α :=
  generateFrom { s : Set α | ∃ a : α, s = { b : α | a < b } ∨ s = { b : α | b < a } }
#align preorder.topology Preorder.topology

section OrderTopology

section Preorder

variable [TopologicalSpace α] [Preorder α] [t : OrderTopology α]

instance : OrderTopology αᵒᵈ :=
  ⟨by
    convert OrderTopology.topology_eq_generate_intervals (α := α) using 6
    apply or_comm⟩

theorem isOpen_iff_generate_intervals {s : Set α} :
    IsOpen s ↔ GenerateOpen { s | ∃ a, s = Ioi a ∨ s = Iio a } s := by
  rw [t.topology_eq_generate_intervals]; rfl
#align is_open_iff_generate_intervals isOpen_iff_generate_intervals

theorem isOpen_lt' (a : α) : IsOpen { b : α | a < b } :=
  isOpen_iff_generate_intervals.2 <| .basic _ ⟨a, .inl rfl⟩
#align is_open_lt' isOpen_lt'

theorem isOpen_gt' (a : α) : IsOpen { b : α | b < a } :=
  isOpen_iff_generate_intervals.2 <| .basic _ ⟨a, .inr rfl⟩
#align is_open_gt' isOpen_gt'

theorem lt_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 b, a < x :=
  (isOpen_lt' _).mem_nhds h
#align lt_mem_nhds lt_mem_nhds

theorem le_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 b, a ≤ x :=
  (lt_mem_nhds h).mono fun _ => le_of_lt
#align le_mem_nhds le_mem_nhds

theorem gt_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 a, x < b :=
  (isOpen_gt' _).mem_nhds h
#align gt_mem_nhds gt_mem_nhds

theorem ge_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 a, x ≤ b :=
  (gt_mem_nhds h).mono fun _ => le_of_lt
#align ge_mem_nhds ge_mem_nhds

theorem nhds_eq_order (a : α) : 𝓝 a = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) := by
  rw [t.topology_eq_generate_intervals, nhds_generateFrom]
  simp_rw [mem_setOf_eq, @and_comm (a ∈ _), exists_or, or_and_right, iInf_or, iInf_and, iInf_exists,
    iInf_inf_eq, iInf_comm (ι := Set α), iInf_iInf_eq_left, mem_Ioi, mem_Iio]
#align nhds_eq_order nhds_eq_order

theorem tendsto_order {f : β → α} {a : α} {x : Filter β} :
    Tendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ b in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ b in x, f b < a' := by
  simp only [nhds_eq_order a, tendsto_inf, tendsto_iInf, tendsto_principal]; rfl
#align tendsto_order tendsto_order

instance tendstoIccClassNhds (a : α) : TendstoIxxClass Icc (𝓝 a) (𝓝 a) := by
  simp only [nhds_eq_order, iInf_subtype']
  refine
    ((hasBasis_iInf_principal_finite _).inf (hasBasis_iInf_principal_finite _)).tendstoIxxClass
      fun s _ => ?_
  refine' ((ordConnected_biInter _).inter (ordConnected_biInter _)).out <;> intro _ _
  exacts [ordConnected_Ioi, ordConnected_Iio]
#align tendsto_Icc_class_nhds tendstoIccClassNhds

instance tendstoIcoClassNhds (a : α) : TendstoIxxClass Ico (𝓝 a) (𝓝 a) :=
  tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self
#align tendsto_Ico_class_nhds tendstoIcoClassNhds

instance tendstoIocClassNhds (a : α) : TendstoIxxClass Ioc (𝓝 a) (𝓝 a) :=
  tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self
#align tendsto_Ioc_class_nhds tendstoIocClassNhds

instance tendstoIooClassNhds (a : α) : TendstoIxxClass Ioo (𝓝 a) (𝓝 a) :=
  tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Icc_self
#align tendsto_Ioo_class_nhds tendstoIooClassNhds

/-- **Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities
hold eventually for the filter. -/
theorem tendsto_of_tendsto_of_tendsto_of_le_of_le' {f g h : β → α} {b : Filter β} {a : α}
    (hg : Tendsto g b (𝓝 a)) (hh : Tendsto h b (𝓝 a)) (hgf : ∀ᶠ b in b, g b ≤ f b)
    (hfh : ∀ᶠ b in b, f b ≤ h b) : Tendsto f b (𝓝 a) :=
  (hg.Icc hh).of_smallSets <| hgf.and hfh
#align tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_of_tendsto_of_tendsto_of_le_of_le'

/-- **Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities
hold everywhere. -/
theorem tendsto_of_tendsto_of_tendsto_of_le_of_le {f g h : β → α} {b : Filter β} {a : α}
    (hg : Tendsto g b (𝓝 a)) (hh : Tendsto h b (𝓝 a)) (hgf : g ≤ f) (hfh : f ≤ h) :
    Tendsto f b (𝓝 a) :=
  tendsto_of_tendsto_of_tendsto_of_le_of_le' hg hh (eventually_of_forall hgf)
    (eventually_of_forall hfh)
#align tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_of_tendsto_of_tendsto_of_le_of_le

theorem nhds_order_unbounded {a : α} (hu : ∃ u, a < u) (hl : ∃ l, l < a) :
    𝓝 a = ⨅ (l) (_ : l < a) (u) (_ : a < u), 𝓟 (Ioo l u) := by
  simp only [nhds_eq_order, ← inf_biInf, ← biInf_inf, *, ← inf_principal, ← Ioi_inter_Iio]; rfl
#align nhds_order_unbounded nhds_order_unbounded

theorem tendsto_order_unbounded {f : β → α} {a : α} {x : Filter β} (hu : ∃ u, a < u)
    (hl : ∃ l, l < a) (h : ∀ l u, l < a → a < u → ∀ᶠ b in x, l < f b ∧ f b < u) :
    Tendsto f x (𝓝 a) := by
  simp only [nhds_order_unbounded hu hl, tendsto_iInf, tendsto_principal]
  exact fun l hl u => h l u hl
#align tendsto_order_unbounded tendsto_order_unbounded

end Preorder

instance tendstoIxxNhdsWithin {α : Type*} [Preorder α] [TopologicalSpace α] (a : α) {s t : Set α}
    {Ixx} [TendstoIxxClass Ixx (𝓝 a) (𝓝 a)] [TendstoIxxClass Ixx (𝓟 s) (𝓟 t)] :
    TendstoIxxClass Ixx (𝓝[s] a) (𝓝[t] a) :=
  Filter.tendstoIxxClass_inf
#align tendsto_Ixx_nhds_within tendstoIxxNhdsWithin

instance tendstoIccClassNhdsPi {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)]
    [∀ i, TopologicalSpace (α i)] [∀ i, OrderTopology (α i)] (f : ∀ i, α i) :
    TendstoIxxClass Icc (𝓝 f) (𝓝 f) := by
  constructor
  conv in (𝓝 f).smallSets => rw [nhds_pi, Filter.pi]
  simp only [smallSets_iInf, smallSets_comap, tendsto_iInf, tendsto_lift', (· ∘ ·),
    mem_powerset_iff]
  intro i s hs
  have : Tendsto (fun g : ∀ i, α i => g i) (𝓝 f) (𝓝 (f i)) := (continuous_apply i).tendsto f
  refine' (tendsto_lift'.1 ((this.comp tendsto_fst).Icc (this.comp tendsto_snd)) s hs).mono _
  exact fun p hp g hg => hp ⟨hg.1 _, hg.2 _⟩
#align tendsto_Icc_class_nhds_pi tendstoIccClassNhdsPi

-- porting note: new lemma
theorem induced_topology_le_preorder [Preorder α] [Preorder β] [TopologicalSpace β]
    [OrderTopology β] {f : α → β} (hf : ∀ {x y}, f x < f y ↔ x < y) :
    induced f ‹TopologicalSpace β› ≤ Preorder.topology α := by
  let _ := Preorder.topology α; have : OrderTopology α := ⟨rfl⟩
  refine le_of_nhds_le_nhds fun x => ?_
  simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal, Ioi, Iio, ← hf]
  refine inf_le_inf (le_iInf₂ fun a ha => ?_) (le_iInf₂ fun a ha => ?_)
  exacts [iInf₂_le (f a) ha, iInf₂_le (f a) ha]

-- porting note: new lemma
theorem induced_topology_eq_preorder [Preorder α] [Preorder β] [TopologicalSpace β]
    [OrderTopology β] {f : α → β} (hf : ∀ {x y}, f x < f y ↔ x < y)
    (H₁ : ∀ {a b x}, b < f a → ¬(b < f x) → ∃ y, y < a ∧ b ≤ f y)
    (H₂ : ∀ {a b x}, f a < b → ¬(f x < b) → ∃ y, a < y ∧ f y ≤ b) :
    induced f ‹TopologicalSpace β› = Preorder.topology α := by
  let _ := Preorder.topology α; have : OrderTopology α := ⟨rfl⟩
  refine le_antisymm (induced_topology_le_preorder hf) ?_
  refine le_of_nhds_le_nhds fun a => ?_
  simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal]
  refine inf_le_inf (le_iInf₂ fun b hb => ?_) (le_iInf₂ fun b hb => ?_)
  · rcases em (∃ x, ¬(b < f x)) with (⟨x, hx⟩ | hb)
    · rcases H₁ hb hx with ⟨y, hya, hyb⟩
      exact iInf₂_le_of_le y hya (principal_mono.2 fun z hz => hyb.trans_lt (hf.2 hz))
    · push_neg at hb
      exact le_principal_iff.2 (univ_mem' hb)
  · rcases em (∃ x, ¬(f x < b)) with (⟨x, hx⟩ | hb)
    · rcases H₂ hb hx with ⟨y, hya, hyb⟩
      exact iInf₂_le_of_le y hya (principal_mono.2 fun z hz => (hf.2 hz).trans_le hyb)
    · push_neg at hb
      exact le_principal_iff.2 (univ_mem' hb)

theorem induced_orderTopology' {α : Type u} {β : Type v} [Preorder α] [ta : TopologicalSpace β]
    [Preorder β] [OrderTopology β] (f : α → β) (hf : ∀ {x y}, f x < f y ↔ x < y)
    (H₁ : ∀ {a x}, x < f a → ∃ b < a, x ≤ f b) (H₂ : ∀ {a x}, f a < x → ∃ b > a, f b ≤ x) :
    @OrderTopology _ (induced f ta) _ :=
  let _ := induced f ta
  ⟨induced_topology_eq_preorder hf (fun h _ => H₁ h) (fun h _ => H₂ h)⟩
#align induced_order_topology' induced_orderTopology'

theorem induced_orderTopology {α : Type u} {β : Type v} [Preorder α] [ta : TopologicalSpace β]
    [Preorder β] [OrderTopology β] (f : α → β) (hf : ∀ {x y}, f x < f y ↔ x < y)
    (H : ∀ {x y}, x < y → ∃ a, x < f a ∧ f a < y) : @OrderTopology _ (induced f ta) _ :=
  induced_orderTopology' f (hf)
    (fun xa => let ⟨b, xb, ba⟩ := H xa; ⟨b, hf.1 ba, le_of_lt xb⟩)
    fun ax => let ⟨b, ab, bx⟩ := H ax; ⟨b, hf.1 ab, le_of_lt bx⟩
#align induced_order_topology induced_orderTopology

/-- The topology induced by a strictly monotone function with order-connected range is the preorder
topology. -/
nonrec theorem StrictMono.induced_topology_eq_preorder {α β : Type*} [LinearOrder α]
    [LinearOrder β] [t : TopologicalSpace β] [OrderTopology β] {f : α → β}
    (hf : StrictMono f) (hc : OrdConnected (range f)) : t.induced f = Preorder.topology α := by
  refine induced_topology_eq_preorder hf.lt_iff_lt (fun h₁ h₂ => ?_) fun h₁ h₂ => ?_
  · rcases hc.out (mem_range_self _) (mem_range_self _) ⟨not_lt.1 h₂, h₁.le⟩ with ⟨y, rfl⟩
    exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩
  · rcases hc.out (mem_range_self _) (mem_range_self _) ⟨h₁.le, not_lt.1 h₂⟩ with ⟨y, rfl⟩
    exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩

/-- A strictly monotone function between linear orders with order topology is a topological
embedding provided that the range of `f` is order-connected. -/
theorem StrictMono.embedding_of_ordConnected {α β : Type*} [LinearOrder α] [LinearOrder β]
    [TopologicalSpace α] [h : OrderTopology α] [TopologicalSpace β] [OrderTopology β] {f : α → β}
    (hf : StrictMono f) (hc : OrdConnected (range f)) : Embedding f :=
  ⟨⟨h.1.trans <| Eq.symm <| hf.induced_topology_eq_preorder hc⟩, hf.injective⟩

/-- On a `Set.OrdConnected` subset of a linear order, the order topology for the restriction of the
order is the same as the restriction to the subset of the order topology. -/
instance orderTopology_of_ordConnected {α : Type u} [TopologicalSpace α] [LinearOrder α]
    [OrderTopology α] {t : Set α} [ht : OrdConnected t] : OrderTopology t :=
  ⟨(Subtype.strictMono_coe t).induced_topology_eq_preorder $ by
    rwa [← @Subtype.range_val _ t] at ht⟩
#align order_topology_of_ord_connected orderTopology_of_ordConnected

theorem nhdsWithin_Ici_eq'' [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
    𝓝[≥] a = (⨅ (u) (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) := by
  rw [nhdsWithin, nhds_eq_order]
  refine' le_antisymm (inf_le_inf_right _ inf_le_right) (le_inf (le_inf _ inf_le_left) inf_le_right)
  exact inf_le_right.trans (le_iInf₂ fun l hl => principal_mono.2 <| Ici_subset_Ioi.2 hl)
#align nhds_within_Ici_eq'' nhdsWithin_Ici_eq''

theorem nhdsWithin_Iic_eq'' [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
    𝓝[≤] a = (⨅ l < a, 𝓟 (Ioi l)) ⊓ 𝓟 (Iic a) :=
  nhdsWithin_Ici_eq'' (toDual a)
#align nhds_within_Iic_eq'' nhdsWithin_Iic_eq''

theorem nhdsWithin_Ici_eq' [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α}
    (ha : ∃ u, a < u) : 𝓝[≥] a = ⨅ (u) (_ : a < u), 𝓟 (Ico a u) := by
  simp only [nhdsWithin_Ici_eq'', biInf_inf ha, inf_principal, Iio_inter_Ici]
#align nhds_within_Ici_eq' nhdsWithin_Ici_eq'

theorem nhdsWithin_Iic_eq' [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α}
    (ha : ∃ l, l < a) : 𝓝[≤] a = ⨅ l < a, 𝓟 (Ioc l a) := by
  simp only [nhdsWithin_Iic_eq'', biInf_inf ha, inf_principal, Ioi_inter_Iic]
#align nhds_within_Iic_eq' nhdsWithin_Iic_eq'

theorem nhdsWithin_Ici_basis' [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α}
    (ha : ∃ u, a < u) : (𝓝[≥] a).HasBasis (fun u => a < u) fun u => Ico a u :=
  (nhdsWithin_Ici_eq' ha).symm ▸
    hasBasis_biInf_principal
      (fun b hb c hc => ⟨min b c, lt_min hb hc, Ico_subset_Ico_right (min_le_left _ _),
        Ico_subset_Ico_right (min_le_right _ _)⟩)
      ha
#align nhds_within_Ici_basis' nhdsWithin_Ici_basis'

theorem nhdsWithin_Iic_basis' [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α}
    (ha : ∃ l, l < a) : (𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a := by
  convert nhdsWithin_Ici_basis' (α := αᵒᵈ) ha using 2
  exact dual_Ico.symm
#align nhds_within_Iic_basis' nhdsWithin_Iic_basis'

theorem nhdsWithin_Ici_basis [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α]
    (a : α) : (𝓝[≥] a).HasBasis (fun u => a < u) fun u => Ico a u :=
  nhdsWithin_Ici_basis' (exists_gt a)
#align nhds_within_Ici_basis nhdsWithin_Ici_basis

theorem nhdsWithin_Iic_basis [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α]
    (a : α) : (𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a :=
  nhdsWithin_Iic_basis' (exists_lt a)
#align nhds_within_Iic_basis nhdsWithin_Iic_basis

theorem nhds_top_order [TopologicalSpace α] [Preorder α] [OrderTop α] [OrderTopology α] :
    𝓝 (⊤ : α) = ⨅ (l) (h₂ : l < ⊤), 𝓟 (Ioi l) := by simp [nhds_eq_order (⊤ : α)]
#align nhds_top_order nhds_top_order

theorem nhds_bot_order [TopologicalSpace α] [Preorder α] [OrderBot α] [OrderTopology α] :
    𝓝 (⊥ : α) = ⨅ (l) (h₂ : ⊥ < l), 𝓟 (Iio l) := by simp [nhds_eq_order (⊥ : α)]
#align nhds_bot_order nhds_bot_order

theorem nhds_top_basis [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α]
    [Nontrivial α] : (𝓝 ⊤).HasBasis (fun a : α => a < ⊤) fun a : α => Ioi a := by
  have : ∃ x : α, x < ⊤ := (exists_ne ⊤).imp fun x hx => hx.lt_top
  simpa only [Iic_top, nhdsWithin_univ, Ioc_top] using nhdsWithin_Iic_basis' this
#align nhds_top_basis nhds_top_basis

theorem nhds_bot_basis [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α]
    [Nontrivial α] : (𝓝 ⊥).HasBasis (fun a : α => ⊥ < a) fun a : α => Iio a :=
  nhds_top_basis (α := αᵒᵈ)
#align nhds_bot_basis nhds_bot_basis

theorem nhds_top_basis_Ici [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α]
    [Nontrivial α] [DenselyOrdered α] : (𝓝 ⊤).HasBasis (fun a : α => a < ⊤) Ici :=
  nhds_top_basis.to_hasBasis
    (fun _a ha => let ⟨b, hab, hb⟩ := exists_between ha; ⟨b, hb, Ici_subset_Ioi.mpr hab⟩)
    fun a ha => ⟨a, ha, Ioi_subset_Ici_self⟩
#align nhds_top_basis_Ici nhds_top_basis_Ici

theorem nhds_bot_basis_Iic [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α]
    [Nontrivial α] [DenselyOrdered α] : (𝓝 ⊥).HasBasis (fun a : α => ⊥ < a) Iic :=
  nhds_top_basis_Ici (α := αᵒᵈ)
#align nhds_bot_basis_Iic nhds_bot_basis_Iic

theorem tendsto_nhds_top_mono [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β]
    {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊤)) (hg : f ≤ᶠ[l] g) : Tendsto g l (𝓝 ⊤) := by
  simp only [nhds_top_order, tendsto_iInf, tendsto_principal] at hf ⊢
  intro x hx
  filter_upwards [hf x hx, hg] with _ using lt_of_lt_of_le
#align tendsto_nhds_top_mono tendsto_nhds_top_mono

theorem tendsto_nhds_bot_mono [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β]
    {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊥)) (hg : g ≤ᶠ[l] f) : Tendsto g l (𝓝 ⊥) :=
  tendsto_nhds_top_mono (β := βᵒᵈ) hf hg
#align tendsto_nhds_bot_mono tendsto_nhds_bot_mono

theorem tendsto_nhds_top_mono' [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β]
    {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊤)) (hg : f ≤ g) : Tendsto g l (𝓝 ⊤) :=
  tendsto_nhds_top_mono hf (eventually_of_forall hg)
#align tendsto_nhds_top_mono' tendsto_nhds_top_mono'

theorem tendsto_nhds_bot_mono' [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β]
    {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊥)) (hg : g ≤ f) : Tendsto g l (𝓝 ⊥) :=
  tendsto_nhds_bot_mono hf (eventually_of_forall hg)
#align tendsto_nhds_bot_mono' tendsto_nhds_bot_mono'

section LinearOrder

variable [TopologicalSpace α] [LinearOrder α]

section OrderClosedTopology

variable [OrderClosedTopology α] {a b : α}

theorem eventually_le_nhds (hab : a < b) : ∀ᶠ x in 𝓝 a, x ≤ b := Iic_mem_nhds hab
#align eventually_le_nhds eventually_le_nhds

theorem eventually_lt_nhds (hab : a < b) : ∀ᶠ x in 𝓝 a, x < b := Iio_mem_nhds hab
#align eventually_lt_nhds eventually_lt_nhds

theorem eventually_ge_nhds (hab : b < a) : ∀ᶠ x in 𝓝 a, b ≤ x := Ici_mem_nhds hab
#align eventually_ge_nhds eventually_ge_nhds

theorem eventually_gt_nhds (hab : b < a) : ∀ᶠ x in 𝓝 a, b < x := Ioi_mem_nhds hab
#align eventually_gt_nhds eventually_gt_nhds

end OrderClosedTopology

section OrderTopology

variable [OrderTopology α]

theorem order_separated {a₁ a₂ : α} (h : a₁ < a₂) :
    ∃ u v : Set α, IsOpen u ∧ IsOpen v ∧ a₁ ∈ u ∧ a₂ ∈ v ∧ ∀ b₁ ∈ u, ∀ b₂ ∈ v, b₁ < b₂ :=
  let ⟨x, hx, y, hy, h⟩ := h.exists_disjoint_Iio_Ioi
  ⟨Iio x, Ioi y, isOpen_gt' _, isOpen_lt' _, hx, hy, h⟩
#align order_separated order_separated

-- see Note [lower instance priority]
instance (priority := 100) OrderTopology.to_orderClosedTopology : OrderClosedTopology α where
  isClosed_le' := isOpen_compl_iff.1 <| isOpen_prod_iff.mpr fun a₁ a₂ (h : ¬a₁ ≤ a₂) =>
    have h : a₂ < a₁ := lt_of_not_ge h
    let ⟨u, v, hu, hv, ha₁, ha₂, h⟩ := order_separated h
    ⟨v, u, hv, hu, ha₂, ha₁, fun ⟨b₁, b₂⟩ ⟨h₁, h₂⟩ => not_le_of_gt <| h b₂ h₂ b₁ h₁⟩
#align order_topology.to_order_closed_topology OrderTopology.to_orderClosedTopology

theorem exists_Ioc_subset_of_mem_nhds {a : α} {s : Set α} (hs : s ∈ 𝓝 a) (h : ∃ l, l < a) :
    ∃ l < a, Ioc l a ⊆ s :=
  (nhdsWithin_Iic_basis' h).mem_iff.mp (nhdsWithin_le_nhds hs)
#align exists_Ioc_subset_of_mem_nhds exists_Ioc_subset_of_mem_nhds

theorem exists_Ioc_subset_of_mem_nhds' {a : α} {s : Set α} (hs : s ∈ 𝓝 a) {l : α} (hl : l < a) :
    ∃ l' ∈ Ico l a, Ioc l' a ⊆ s :=
  let ⟨l', hl'a, hl's⟩ := exists_Ioc_subset_of_mem_nhds hs ⟨l, hl⟩
  ⟨max l l', ⟨le_max_left _ _, max_lt hl hl'a⟩,
    (Ioc_subset_Ioc_left <| le_max_right _ _).trans hl's⟩
#align exists_Ioc_subset_of_mem_nhds' exists_Ioc_subset_of_mem_nhds'

theorem exists_Ico_subset_of_mem_nhds' {a : α} {s : Set α} (hs : s ∈ 𝓝 a) {u : α} (hu : a < u) :
    ∃ u' ∈ Ioc a u, Ico a u' ⊆ s := by
  simpa only [OrderDual.exists, exists_prop, dual_Ico, dual_Ioc] using
    exists_Ioc_subset_of_mem_nhds' (show ofDual ⁻¹' s ∈ 𝓝 (toDual a) from hs) hu.dual
#align exists_Ico_subset_of_mem_nhds' exists_Ico_subset_of_mem_nhds'

theorem exists_Ico_subset_of_mem_nhds {a : α} {s : Set α} (hs : s ∈ 𝓝 a) (h : ∃ u, a < u) :
    ∃ u, a < u ∧ Ico a u ⊆ s :=
  let ⟨_l', hl'⟩ := h;
  let ⟨l, hl⟩ := exists_Ico_subset_of_mem_nhds' hs hl'
  ⟨l, hl.1.1, hl.2⟩
#align exists_Ico_subset_of_mem_nhds exists_Ico_subset_of_mem_nhds

theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Ici {a : α} {s : Set α} (hs : s ∈ 𝓝[≥] a) :
    ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s := by
  rcases (em (IsMax a)).imp_right not_isMax_iff.mp with (ha | ha)
  · use a
    simpa [ha.Ici_eq] using hs
  · rcases (nhdsWithin_Ici_basis' ha).mem_iff.mp hs with ⟨b, hab, hbs⟩
    rcases eq_empty_or_nonempty (Ioo a b) with (H | ⟨c, hac, hcb⟩)
    · have : Ico a b = Icc a a := by rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
      exact ⟨a, le_rfl, this ▸ ⟨Ico_mem_nhdsWithin_Ici' hab, hbs⟩⟩
    · refine' ⟨c, hac.le, Icc_mem_nhdsWithin_Ici' hac, _⟩
      exact (Icc_subset_Ico_right hcb).trans hbs
#align exists_Icc_mem_subset_of_mem_nhds_within_Ici exists_Icc_mem_subset_of_mem_nhdsWithin_Ici

theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Iic {a : α} {s : Set α} (hs : s ∈ 𝓝[≤] a) :
    ∃ b ≤ a, Icc b a ∈ 𝓝[≤] a ∧ Icc b a ⊆ s := by
  simpa only [dual_Icc, toDual.surjective.exists] using
    exists_Icc_mem_subset_of_mem_nhdsWithin_Ici (α := αᵒᵈ) (a := toDual a) hs
#align exists_Icc_mem_subset_of_mem_nhds_within_Iic exists_Icc_mem_subset_of_mem_nhdsWithin_Iic

theorem exists_Icc_mem_subset_of_mem_nhds {a : α} {s : Set α} (hs : s ∈ 𝓝 a) :
    ∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s := by
  rcases exists_Icc_mem_subset_of_mem_nhdsWithin_Iic (nhdsWithin_le_nhds hs) with
    ⟨b, hba, hb_nhds, hbs⟩
  rcases exists_Icc_mem_subset_of_mem_nhdsWithin_Ici (nhdsWithin_le_nhds hs) with
    ⟨c, hac, hc_nhds, hcs⟩
  refine' ⟨b, c, ⟨hba, hac⟩, _⟩
  rw [← Icc_union_Icc_eq_Icc hba hac, ← nhds_left_sup_nhds_right]
  exact ⟨union_mem_sup hb_nhds hc_nhds, union_subset hbs hcs⟩
#align exists_Icc_mem_subset_of_mem_nhds exists_Icc_mem_subset_of_mem_nhds

theorem IsOpen.exists_Ioo_subset [Nontrivial α] {s : Set α} (hs : IsOpen s) (h : s.Nonempty) :
    ∃ a b, a < b ∧ Ioo a b ⊆ s := by
  obtain ⟨x, hx⟩ : ∃ x, x ∈ s := h
  obtain ⟨y, hy⟩ : ∃ y, y ≠ x := exists_ne x
  rcases lt_trichotomy x y with (H | rfl | H)
  · obtain ⟨u, xu, hu⟩ : ∃ u, x < u ∧ Ico x u ⊆ s :=
      exists_Ico_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩
    exact ⟨x, u, xu, Ioo_subset_Ico_self.trans hu⟩
  · exact (hy rfl).elim
  · obtain ⟨l, lx, hl⟩ : ∃ l, l < x ∧ Ioc l x ⊆ s :=
      exists_Ioc_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩
    exact ⟨l, x, lx, Ioo_subset_Ioc_self.trans hl⟩
#align is_open.exists_Ioo_subset IsOpen.exists_Ioo_subset

theorem dense_of_exists_between [Nontrivial α] {s : Set α}
    (h : ∀ ⦃a b⦄, a < b → ∃ c ∈ s, a < c ∧ c < b) : Dense s := by
  refine dense_iff_inter_open.2 fun U U_open U_nonempty => ?_
  obtain ⟨a, b, hab, H⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ U := U_open.exists_Ioo_subset U_nonempty
  obtain ⟨x, xs, hx⟩ : ∃ x ∈ s, a < x ∧ x < b := h hab
  exact ⟨x, ⟨H hx, xs⟩⟩
#align dense_of_exists_between dense_of_exists_between

/-- A set in a nontrivial densely linear ordered type is dense in the sense of topology if and only
if for any `a < b` there exists `c ∈ s`, `a < c < b`. Each implication requires less typeclass
assumptions. -/
theorem dense_iff_exists_between [DenselyOrdered α] [Nontrivial α] {s : Set α} :
    Dense s ↔ ∀ a b, a < b → ∃ c ∈ s, a < c ∧ c < b :=
  ⟨fun h _ _ hab => h.exists_between hab, dense_of_exists_between⟩
#align dense_iff_exists_between dense_iff_exists_between

/-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`,
provided `a` is neither a bottom element nor a top element. -/
theorem mem_nhds_iff_exists_Ioo_subset' {a : α} {s : Set α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) :
    s ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s := by
  constructor
  · intro h
    rcases exists_Ico_subset_of_mem_nhds h hu with ⟨u, au, hu⟩
    rcases exists_Ioc_subset_of_mem_nhds h hl with ⟨l, la, hl⟩
    exact ⟨l, u, ⟨la, au⟩, Ioc_union_Ico_eq_Ioo la au ▸ union_subset hl hu⟩
  · rintro ⟨l, u, ha, h⟩
    apply mem_of_superset (Ioo_mem_nhds ha.1 ha.2) h
#align mem_nhds_iff_exists_Ioo_subset' mem_nhds_iff_exists_Ioo_subset'

/-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`.
-/
theorem mem_nhds_iff_exists_Ioo_subset [NoMaxOrder α] [NoMinOrder α] {a : α} {s : Set α} :
    s ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s :=
  mem_nhds_iff_exists_Ioo_subset' (exists_lt a) (exists_gt a)
#align mem_nhds_iff_exists_Ioo_subset mem_nhds_iff_exists_Ioo_subset

theorem nhds_basis_Ioo' {a : α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) :
    (𝓝 a).HasBasis (fun b : α × α => b.1 < a ∧ a < b.2) fun b => Ioo b.1 b.2 :=
  ⟨fun s => (mem_nhds_iff_exists_Ioo_subset' hl hu).trans <| by simp⟩
#align nhds_basis_Ioo' nhds_basis_Ioo'

theorem nhds_basis_Ioo [NoMaxOrder α] [NoMinOrder α] (a : α) :
    (𝓝 a).HasBasis (fun b : α × α => b.1 < a ∧ a < b.2) fun b => Ioo b.1 b.2 :=
  nhds_basis_Ioo' (exists_lt a) (exists_gt a)
#align nhds_basis_Ioo nhds_basis_Ioo

theorem Filter.Eventually.exists_Ioo_subset [NoMaxOrder α] [NoMinOrder α] {a : α} {p : α → Prop}
    (hp : ∀ᶠ x in 𝓝 a, p x) : ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ { x | p x } :=
  mem_nhds_iff_exists_Ioo_subset.1 hp
#align filter.eventually.exists_Ioo_subset Filter.Eventually.exists_Ioo_subset

theorem Dense.topology_eq_generateFrom [DenselyOrdered α] {s : Set α} (hs : Dense s) :
    ‹TopologicalSpace α› = .generateFrom (Ioi '' s ∪ Iio '' s) := by
  refine (OrderTopology.topology_eq_generate_intervals (α := α)).trans ?_
  refine le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)
  · simp only [union_subset_iff, image_subset_iff]
    exact ⟨fun a _ ↦ ⟨a, .inl rfl⟩, fun a _ ↦ ⟨a, .inr rfl⟩⟩
  · rintro _ ⟨a, rfl | rfl⟩
    · rw [hs.Ioi_eq_biUnion]
      let _ := generateFrom (Ioi '' s ∪ Iio '' s)
      exact isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inl <| mem_image_of_mem _ h.1
    · rw [hs.Iio_eq_biUnion]
      let _ := generateFrom (Ioi '' s ∪ Iio '' s)
      exact isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inr <| mem_image_of_mem _ h.1

variable (α)

/-- Let `α` be a densely ordered linear order with order topology. If `α` is a separable space, then
it has second countable topology. Note that the "densely ordered" assumption cannot be dropped, see
[double arrow space](https://topology.pi-base.org/spaces/S000093) for a counterexample. -/
theorem TopologicalSpace.SecondCountableTopology.of_separableSpace_orderTopology [DenselyOrdered α]
    [SeparableSpace α] : SecondCountableTopology α := by
  rcases exists_countable_dense α with ⟨s, hc, hd⟩
  refine ⟨⟨_, ?_, hd.topology_eq_generateFrom⟩⟩
  exact (hc.image _).union (hc.image _)

variable {α}

-- porting note: new lemma
/-- The set of points which are isolated on the right is countable when the space is
second-countable. -/
theorem countable_setOf_covby_right [SecondCountableTopology α] :
    Set.Countable { x : α | ∃ y, x ⋖ y } := by
  nontriviality α
  let s := { x : α | ∃ y, x ⋖ y }
  have : ∀ x ∈ s, ∃ y, x ⋖ y := fun x => id
  choose! y hy using this
  have Hy : ∀ x z, x ∈ s → z < y x → z ≤ x := fun x z hx => (hy x hx).le_of_lt
  suffices H : ∀ a : Set α, IsOpen a → Set.Countable { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a }
  · have : s ⊆ ⋃ a ∈ countableBasis α, { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a } := fun x hx => by
      rcases (isBasis_countableBasis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩
      exact mem_iUnion₂.2 ⟨a, ab, hx, xa, ya⟩
    refine Set.Countable.mono this ?_
    refine' Countable.biUnion (countable_countableBasis α) fun a ha => H _ _
    exact isOpen_of_mem_countableBasis ha
  intro a ha
  suffices H : Set.Countable { x | (x ∈ s ∧ x ∈ a ∧ y x ∉ a) ∧ ¬IsBot x }
  · exact H.of_diff (subsingleton_isBot α).countable
  simp only [and_assoc]
  let t := { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x }
  have : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a := by
    intro x hx
    apply exists_Ioc_subset_of_mem_nhds (ha.mem_nhds hx.2.1)
    simpa only [IsBot, not_forall, not_le] using hx.right.right.right
  choose! z hz h'z using this
  have : PairwiseDisjoint t fun x => Ioc (z x) x := fun x xt x' x't hxx' => by
    rcases hxx'.lt_or_lt with (h' | h')
    · refine' disjoint_left.2 fun u ux ux' => xt.2.2.1 _
      refine' h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), _⟩
      by_contra' H
      exact lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h')
    · refine' disjoint_left.2 fun u ux ux' => x't.2.2.1 _
      refine' h'z x xt ⟨ux.1.trans_le (ux'.2.trans (hy x' x't.1).le), _⟩
      by_contra' H
      exact lt_irrefl _ ((Hy _ _ x't.1 H).trans_lt h')
  refine' this.countable_of_isOpen (fun x hx => _) fun x hx => ⟨x, hz x hx, le_rfl⟩
  suffices H : Ioc (z x) x = Ioo (z x) (y x)
  · rw [H]
    exact isOpen_Ioo
  exact Subset.antisymm (Ioc_subset_Ioo_right (hy x hx.1).lt) fun u hu => ⟨hu.1, Hy _ _ hx.1 hu.2⟩

/-- The set of points which are isolated on the right is countable when the space is
second-countable. -/
@[deprecated countable_setOf_covby_right]
theorem countable_of_isolated_right' [SecondCountableTopology α] :
    Set.Countable { x : α | ∃ y, x < y ∧ Ioo x y = ∅ } := by
  simpa only [← covby_iff_Ioo_eq] using countable_setOf_covby_right
#align countable_of_isolated_right countable_of_isolated_right'

/-- The set of points which are isolated on the left is countable when the space is
second-countable. -/
theorem countable_setOf_covby_left [SecondCountableTopology α] :
    Set.Countable { x : α | ∃ y, y ⋖ x } := by
  convert countable_setOf_covby_right (α := αᵒᵈ) using 5
  exact toDual_covby_toDual_iff.symm

/-- The set of points which are isolated on the left is countable when the space is
second-countable. -/
theorem countable_of_isolated_left' [SecondCountableTopology α] :
    Set.Countable { x : α | ∃ y, y < x ∧ Ioo y x = ∅ } := by
  simpa only [← covby_iff_Ioo_eq] using countable_setOf_covby_left
#align countable_of_isolated_left countable_of_isolated_left'

/-- Consider a disjoint family of intervals `(x, y)` with `x < y` in a second-countable space.
Then the family is countable.
This is not a straightforward consequence of second-countability as some of these intervals might be
empty (but in fact this can happen only for countably many of them). -/
theorem Set.PairwiseDisjoint.countable_of_Ioo [SecondCountableTopology α] {y : α → α} {s : Set α}
    (h : PairwiseDisjoint s fun x => Ioo x (y x)) (h' : ∀ x ∈ s, x < y x) : s.Countable :=
  have : (s \ { x | ∃ y, x ⋖ y }).Countable :=
    (h.subset (diff_subset _ _)).countable_of_isOpen (fun _ _ => isOpen_Ioo)
      fun x hx => (h' _ hx.1).exists_lt_lt (mt (Exists.intro (y x)) hx.2)
  this.of_diff countable_setOf_covby_right
#align set.pairwise_disjoint.countable_of_Ioo Set.PairwiseDisjoint.countable_of_Ioo

instance instIsCountablyGenerated_atTop [SecondCountableTopology α] :
    IsCountablyGenerated (atTop : Filter α) := by
  by_cases h : ∃ (x : α), IsTop x
  · rcases h with ⟨x, hx⟩
    rw [atTop_eq_pure_of_isTop hx]
    exact isCountablyGenerated_pure x
  · rcases exists_countable_basis α with ⟨b, b_count, b_ne, hb⟩
    have : Countable b := by exact Iff.mpr countable_coe_iff b_count
    have A : ∀ (s : b), ∃ (x : α), x ∈ (s : Set α) := by
      intro s
      have : (s : Set α) ≠ ∅ := by
        intro H
        apply b_ne
        convert s.2
        exact H.symm
      exact Iff.mp nmem_singleton_empty this
    choose a ha using A
    have : (atTop : Filter α) = (generate (Ici '' (range a))) := by
      apply atTop_eq_generate_of_not_bddAbove
      intro ⟨x, hx⟩
      simp only [IsTop, not_exists, not_forall, not_le] at h
      rcases h x with ⟨y, hy⟩
      obtain ⟨s, sb, -, hs⟩ : ∃ s, s ∈ b ∧ y ∈ s ∧ s ⊆ Ioi x :=
        hb.exists_subset_of_mem_open hy isOpen_Ioi
      have I : a ⟨s, sb⟩ ≤ x := hx (mem_range_self _)
      have J : x < a ⟨s, sb⟩ := hs (ha ⟨s, sb⟩)
      exact lt_irrefl _ (I.trans_lt J)
    rw [this]
    exact ⟨_, (countable_range _).image _, rfl⟩

instance instIsCountablyGenerated_atBot [SecondCountableTopology α] :
    IsCountablyGenerated (atBot : Filter α) :=
  @instIsCountablyGenerated_atTop αᵒᵈ _ _ _ _

section Pi

/-!
### Intervals in `Π i, π i` belong to `𝓝 x`

For each lemma `pi_Ixx_mem_nhds` we add a non-dependent version `pi_Ixx_mem_nhds'` because
sometimes Lean fails to unify different instances while trying to apply the dependent version to,
e.g., `ι → ℝ`.
-/

variable {ι : Type*} {π : ι → Type*} [Finite ι] [∀ i, LinearOrder (π i)]
  [∀ i, TopologicalSpace (π i)] [∀ i, OrderTopology (π i)] {a b x : ∀ i, π i} {a' b' x' : ι → α}

theorem pi_Iic_mem_nhds (ha : ∀ i, x i < a i) : Iic a ∈ 𝓝 x :=
  pi_univ_Iic a ▸ set_pi_mem_nhds (Set.toFinite _) fun _ _ => Iic_mem_nhds (ha _)
#align pi_Iic_mem_nhds pi_Iic_mem_nhds

theorem pi_Iic_mem_nhds' (ha : ∀ i, x' i < a' i) : Iic a' ∈ 𝓝 x' :=
  pi_Iic_mem_nhds ha
#align pi_Iic_mem_nhds' pi_Iic_mem_nhds'

theorem pi_Ici_mem_nhds (ha : ∀ i, a i < x i) : Ici a ∈ 𝓝 x :=
  pi_univ_Ici a ▸ set_pi_mem_nhds (Set.toFinite _) fun _ _ => Ici_mem_nhds (ha _)
#align pi_Ici_mem_nhds pi_Ici_mem_nhds

theorem pi_Ici_mem_nhds' (ha : ∀ i, a' i < x' i) : Ici a' ∈ 𝓝 x' :=
  pi_Ici_mem_nhds ha
#align pi_Ici_mem_nhds' pi_Ici_mem_nhds'

theorem pi_Icc_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Icc a b ∈ 𝓝 x :=
  pi_univ_Icc a b ▸ set_pi_mem_nhds finite_univ fun _ _ => Icc_mem_nhds (ha _) (hb _)
#align pi_Icc_mem_nhds pi_Icc_mem_nhds

theorem pi_Icc_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Icc a' b' ∈ 𝓝 x' :=
  pi_Icc_mem_nhds ha hb
#align pi_Icc_mem_nhds' pi_Icc_mem_nhds'

variable [Nonempty ι]

theorem pi_Iio_mem_nhds (ha : ∀ i, x i < a i) : Iio a ∈ 𝓝 x := by
  refine' mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => _) (pi_univ_Iio_subset a)
  exact Iio_mem_nhds (ha i)
#align pi_Iio_mem_nhds pi_Iio_mem_nhds

theorem pi_Iio_mem_nhds' (ha : ∀ i, x' i < a' i) : Iio a' ∈ 𝓝 x' :=
  pi_Iio_mem_nhds ha
#align pi_Iio_mem_nhds' pi_Iio_mem_nhds'

theorem pi_Ioi_mem_nhds (ha : ∀ i, a i < x i) : Ioi a ∈ 𝓝 x :=
  @pi_Iio_mem_nhds ι (fun i => (π i)ᵒᵈ) _ _ _ _ _ _ _ ha
#align pi_Ioi_mem_nhds pi_Ioi_mem_nhds

theorem pi_Ioi_mem_nhds' (ha : ∀ i, a' i < x' i) : Ioi a' ∈ 𝓝 x' :=
  pi_Ioi_mem_nhds ha
#align pi_Ioi_mem_nhds' pi_Ioi_mem_nhds'

theorem pi_Ioc_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ioc a b ∈ 𝓝 x := by
  refine' mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => _) (pi_univ_Ioc_subset a b)
  exact Ioc_mem_nhds (ha i) (hb i)
#align pi_Ioc_mem_nhds pi_Ioc_mem_nhds

theorem pi_Ioc_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Ioc a' b' ∈ 𝓝 x' :=
  pi_Ioc_mem_nhds ha hb
#align pi_Ioc_mem_nhds' pi_Ioc_mem_nhds'

theorem pi_Ico_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ico a b ∈ 𝓝 x := by
  refine' mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => _) (pi_univ_Ico_subset a b)
  exact Ico_mem_nhds (ha i) (hb i)
#align pi_Ico_mem_nhds pi_Ico_mem_nhds

theorem pi_Ico_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Ico a' b' ∈ 𝓝 x' :=
  pi_Ico_mem_nhds ha hb
#align pi_Ico_mem_nhds' pi_Ico_mem_nhds'

theorem pi_Ioo_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ioo a b ∈ 𝓝 x := by
  refine' mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => _) (pi_univ_Ioo_subset a b)
  exact Ioo_mem_nhds (ha i) (hb i)
#align pi_Ioo_mem_nhds pi_Ioo_mem_nhds

theorem pi_Ioo_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Ioo a' b' ∈ 𝓝 x' :=
  pi_Ioo_mem_nhds ha hb
#align pi_Ioo_mem_nhds' pi_Ioo_mem_nhds'

end Pi

theorem disjoint_nhds_atTop [NoMaxOrder α] (x : α) : Disjoint (𝓝 x) atTop := by
  rcases exists_gt x with ⟨y, hy : x < y⟩
  refine' disjoint_of_disjoint_of_mem _ (Iio_mem_nhds hy) (mem_atTop y)
  exact disjoint_left.mpr fun z => not_le.2
#align disjoint_nhds_at_top disjoint_nhds_atTop

@[simp]
theorem inf_nhds_atTop [NoMaxOrder α] (x : α) : 𝓝 x ⊓ atTop = ⊥ :=
  disjoint_iff.1 (disjoint_nhds_atTop x)
#align inf_nhds_at_top inf_nhds_atTop

theorem disjoint_nhds_atBot [NoMinOrder α] (x : α) : Disjoint (𝓝 x) atBot :=
  disjoint_nhds_atTop (α := αᵒᵈ) x
#align disjoint_nhds_at_bot disjoint_nhds_atBot

@[simp]
theorem inf_nhds_atBot [NoMinOrder α] (x : α) : 𝓝 x ⊓ atBot = ⊥ :=
  inf_nhds_atTop (α := αᵒᵈ) x
#align inf_nhds_at_bot inf_nhds_atBot

theorem not_tendsto_nhds_of_tendsto_atTop [NoMaxOrder α] {F : Filter β} [NeBot F] {f : β → α}
    (hf : Tendsto f F atTop) (x : α) : ¬Tendsto f F (𝓝 x) :=
  hf.not_tendsto (disjoint_nhds_atTop x).symm
#align not_tendsto_nhds_of_tendsto_at_top not_tendsto_nhds_of_tendsto_atTop

theorem not_tendsto_atTop_of_tendsto_nhds [NoMaxOrder α] {F : Filter β} [NeBot F] {f : β → α}
    {x : α} (hf : Tendsto f F (𝓝 x)) : ¬Tendsto f F atTop :=
  hf.not_tendsto (disjoint_nhds_atTop x)
#align not_tendsto_at_top_of_tendsto_nhds not_tendsto_atTop_of_tendsto_nhds

theorem not_tendsto_nhds_of_tendsto_atBot [NoMinOrder α] {F : Filter β} [NeBot F] {f : β → α}
    (hf : Tendsto f F atBot) (x : α) : ¬Tendsto f F (𝓝 x) :=
  hf.not_tendsto (disjoint_nhds_atBot x).symm
#align not_tendsto_nhds_of_tendsto_at_bot not_tendsto_nhds_of_tendsto_atBot

theorem not_tendsto_atBot_of_tendsto_nhds [NoMinOrder α] {F : Filter β} [NeBot F] {f : β → α}
    {x : α} (hf : Tendsto f F (𝓝 x)) : ¬Tendsto f F atBot :=
  hf.not_tendsto (disjoint_nhds_atBot x)
#align not_tendsto_at_bot_of_tendsto_nhds not_tendsto_atBot_of_tendsto_nhds

/-!
### Neighborhoods to the left and to the right on an `OrderTopology`

We've seen some properties of left and right neighborhood of a point in an `OrderClosedTopology`.
In an `OrderTopology`, such neighborhoods can be characterized as the sets containing suitable
intervals to the right or to the left of `a`. We give now these characterizations. -/

open List in
/-- The following statements are equivalent:

0. `s` is a neighborhood of `a` within `(a, +∞)`;
1. `s` is a neighborhood of `a` within `(a, b]`;
2. `s` is a neighborhood of `a` within `(a, b)`;
3. `s` includes `(a, u)` for some `u ∈ (a, b]`;
4. `s` includes `(a, u)` for some `u > a`.
-/
theorem TFAE_mem_nhdsWithin_Ioi {a b : α} (hab : a < b) (s : Set α) :
    TFAE [s ∈ 𝓝[>] a,
      s ∈ 𝓝[Ioc a b] a,
      s ∈ 𝓝[Ioo a b] a,
      ∃ u ∈ Ioc a b, Ioo a u ⊆ s,
      ∃ u ∈ Ioi a, Ioo a u ⊆ s] := by
  tfae_have 1 ↔ 2
  · rw [nhdsWithin_Ioc_eq_nhdsWithin_Ioi hab]
  tfae_have 1 ↔ 3
  · rw [nhdsWithin_Ioo_eq_nhdsWithin_Ioi hab]
  tfae_have 4 → 5
  · exact fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩
  tfae_have 5 → 1
  · rintro ⟨u, hau, hu⟩
    exact mem_of_superset (Ioo_mem_nhdsWithin_Ioi ⟨le_refl a, hau⟩) hu
  tfae_have 1 → 4
  · intro h
    rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩
    rcases exists_Ico_subset_of_mem_nhds' va hab with ⟨u, au, hu⟩
    refine' ⟨u, au, fun x hx => _⟩
    refine' hv ⟨hu ⟨le_of_lt hx.1, hx.2⟩, _⟩
    exact hx.1
  tfae_finish
#align tfae_mem_nhds_within_Ioi TFAE_mem_nhdsWithin_Ioi

theorem mem_nhdsWithin_Ioi_iff_exists_mem_Ioc_Ioo_subset {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioc a u', Ioo a u ⊆ s :=
  (TFAE_mem_nhdsWithin_Ioi hu' s).out 0 3
#align mem_nhds_within_Ioi_iff_exists_mem_Ioc_Ioo_subset mem_nhdsWithin_Ioi_iff_exists_mem_Ioc_Ioo_subset

/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)`
with `a < u < u'`, provided `a` is not a top element. -/
theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioo a u ⊆ s :=
  (TFAE_mem_nhdsWithin_Ioi hu' s).out 0 4
#align mem_nhds_within_Ioi_iff_exists_Ioo_subset' mem_nhdsWithin_Ioi_iff_exists_Ioo_subset'

theorem nhdsWithin_Ioi_basis' {a : α} (h : ∃ b, a < b) : (𝓝[>] a).HasBasis (a < ·) (Ioo a) :=
  let ⟨_, h⟩ := h
  ⟨fun _ => mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' h⟩

theorem nhdsWithin_Ioi_eq_bot_iff {a : α} : 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b := by
  by_cases ha : IsTop a
  · simp [ha, ha.isMax.Ioi_eq]
  · simp only [ha, false_or]
    rw [isTop_iff_isMax, not_isMax_iff] at ha
    simp only [(nhdsWithin_Ioi_basis' ha).eq_bot_iff, covby_iff_Ioo_eq]

/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)`
with `a < u`. -/
theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset [NoMaxOrder α] {a : α} {s : Set α} :
    s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioo a u ⊆ s :=
  let ⟨_u', hu'⟩ := exists_gt a
  mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' hu'
#align mem_nhds_within_Ioi_iff_exists_Ioo_subset mem_nhdsWithin_Ioi_iff_exists_Ioo_subset

/-- The set of points which are isolated on the right is countable when the space is
second-countable. -/
theorem countable_setOf_isolated_right [SecondCountableTopology α] :
    { x : α | 𝓝[>] x = ⊥ }.Countable := by
  simp only [nhdsWithin_Ioi_eq_bot_iff, setOf_or]
  exact (subsingleton_isTop α).countable.union countable_setOf_covby_right

/-- The set of points which are isolated on the left is countable when the space is
second-countable. -/
theorem countable_setOf_isolated_left [SecondCountableTopology α] :
    { x : α | 𝓝[<] x = ⊥ }.Countable :=
  countable_setOf_isolated_right (α := αᵒᵈ)

/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u]`
with `a < u`. -/
theorem mem_nhdsWithin_Ioi_iff_exists_Ioc_subset [NoMaxOrder α] [DenselyOrdered α] {a : α}
    {s : Set α} : s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s := by
  rw [mem_nhdsWithin_Ioi_iff_exists_Ioo_subset]
  constructor
  · rintro ⟨u, au, as⟩
    rcases exists_between au with ⟨v, hv⟩
    exact ⟨v, hv.1, fun x hx => as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩
  · rintro ⟨u, au, as⟩
    exact ⟨u, au, Subset.trans Ioo_subset_Ioc_self as⟩
#align mem_nhds_within_Ioi_iff_exists_Ioc_subset mem_nhdsWithin_Ioi_iff_exists_Ioc_subset

open List in
/-- The following statements are equivalent:

0. `s` is a neighborhood of `b` within `(-∞, b)`
1. `s` is a neighborhood of `b` within `[a, b)`
2. `s` is a neighborhood of `b` within `(a, b)`
3. `s` includes `(l, b)` for some `l ∈ [a, b)`
4. `s` includes `(l, b)` for some `l < b` -/
theorem TFAE_mem_nhdsWithin_Iio {a b : α} (h : a < b) (s : Set α) :
    TFAE [s ∈ 𝓝[<] b,-- 0 : `s` is a neighborhood of `b` within `(-∞, b)`
        s ∈ 𝓝[Ico a b] b,-- 1 : `s` is a neighborhood of `b` within `[a, b)`
        s ∈ 𝓝[Ioo a b] b,-- 2 : `s` is a neighborhood of `b` within `(a, b)`
        ∃ l ∈ Ico a b, Ioo l b ⊆ s,-- 3 : `s` includes `(l, b)` for some `l ∈ [a, b)`
        ∃ l ∈ Iio b, Ioo l b ⊆ s] := by-- 4 : `s` includes `(l, b)` for some `l < b`
  simpa only [exists_prop, OrderDual.exists, dual_Ioi, dual_Ioc, dual_Ioo] using
    TFAE_mem_nhdsWithin_Ioi h.dual (ofDual ⁻¹' s)
#align tfae_mem_nhds_within_Iio TFAE_mem_nhdsWithin_Iio

theorem mem_nhdsWithin_Iio_iff_exists_mem_Ico_Ioo_subset {a l' : α} {s : Set α} (hl' : l' < a) :
    s ∈ 𝓝[<] a ↔ ∃ l ∈ Ico l' a, Ioo l a ⊆ s :=
  (TFAE_mem_nhdsWithin_Iio hl' s).out 0 3
#align mem_nhds_within_Iio_iff_exists_mem_Ico_Ioo_subset mem_nhdsWithin_Iio_iff_exists_mem_Ico_Ioo_subset

/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `(l, a)`
with `l < a`, provided `a` is not a bottom element. -/
theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset' {a l' : α} {s : Set α} (hl' : l' < a) :
    s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ioo l a ⊆ s :=
  (TFAE_mem_nhdsWithin_Iio hl' s).out 0 4
#align mem_nhds_within_Iio_iff_exists_Ioo_subset' mem_nhdsWithin_Iio_iff_exists_Ioo_subset'

/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `(l, a)`
with `l < a`. -/
theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset [NoMinOrder α] {a : α} {s : Set α} :
    s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ioo l a ⊆ s :=
  let ⟨_, h⟩ := exists_lt a
  mem_nhdsWithin_Iio_iff_exists_Ioo_subset' h
#align mem_nhds_within_Iio_iff_exists_Ioo_subset mem_nhdsWithin_Iio_iff_exists_Ioo_subset

/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `[l, a)`
with `l < a`. -/
theorem mem_nhdsWithin_Iio_iff_exists_Ico_subset [NoMinOrder α] [DenselyOrdered α] {a : α}
    {s : Set α} : s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s := by
  have : ofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ _ := mem_nhdsWithin_Ioi_iff_exists_Ioc_subset
  simpa only [OrderDual.exists, exists_prop, dual_Ioc] using this
#align mem_nhds_within_Iio_iff_exists_Ico_subset mem_nhdsWithin_Iio_iff_exists_Ico_subset

theorem nhdsWithin_Iio_basis' {a : α} (h : ∃ b, b < a) : (𝓝[<] a).HasBasis (· < a) (Ioo · a) :=
  let ⟨_, h⟩ := h
  ⟨fun _ => mem_nhdsWithin_Iio_iff_exists_Ioo_subset' h⟩

theorem nhdsWithin_Iio_eq_bot_iff {a : α} : 𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a := by
    convert (config := {preTransparency := .default})
      nhdsWithin_Ioi_eq_bot_iff (a := OrderDual.toDual a) using 4
    exact ofDual_covby_ofDual_iff

open List in
/-- The following statements are equivalent:

0. `s` is a neighborhood of `a` within `[a, +∞)`;
1. `s` is a neighborhood of `a` within `[a, b]`;
2. `s` is a neighborhood of `a` within `[a, b)`;
3. `s` includes `[a, u)` for some `u ∈ (a, b]`;
4. `s` includes `[a, u)` for some `u > a`.
-/
theorem TFAE_mem_nhdsWithin_Ici {a b : α} (hab : a < b) (s : Set α) :
    TFAE [s ∈ 𝓝[≥] a,
      s ∈ 𝓝[Icc a b] a,
      s ∈ 𝓝[Ico a b] a,
      ∃ u ∈ Ioc a b, Ico a u ⊆ s,
      ∃ u ∈ Ioi a , Ico a u ⊆ s] := by
  tfae_have 1 ↔ 2
  · rw [nhdsWithin_Icc_eq_nhdsWithin_Ici hab]
  tfae_have 1 ↔ 3
  · rw [nhdsWithin_Ico_eq_nhdsWithin_Ici hab]
  tfae_have 1 ↔ 5
  · exact (nhdsWithin_Ici_basis' ⟨b, hab⟩).mem_iff
  tfae_have 4 → 5
  · exact fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩
  tfae_have 5 → 4
  · rintro ⟨u, hua, hus⟩
    exact
      ⟨min u b, ⟨lt_min hua hab, min_le_right _ _⟩,
        (Ico_subset_Ico_right <| min_le_left _ _).trans hus⟩
  tfae_finish
#align tfae_mem_nhds_within_Ici TFAE_mem_nhdsWithin_Ici

theorem mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioc a u', Ico a u ⊆ s :=
  (TFAE_mem_nhdsWithin_Ici hu' s).out 0 3 (by norm_num) (by norm_num)
#align mem_nhds_within_Ici_iff_exists_mem_Ioc_Ico_subset mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset

/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u)`
with `a < u < u'`, provided `a` is not a top element. -/
theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset' {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s :=
  (TFAE_mem_nhdsWithin_Ici hu' s).out 0 4 (by norm_num) (by norm_num)
#align mem_nhds_within_Ici_iff_exists_Ico_subset' mem_nhdsWithin_Ici_iff_exists_Ico_subset'

/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u)`
with `a < u`. -/
theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset [NoMaxOrder α] {a : α} {s : Set α} :
    s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s :=
  let ⟨_, hu'⟩ := exists_gt a
  mem_nhdsWithin_Ici_iff_exists_Ico_subset' hu'
#align mem_nhds_within_Ici_iff_exists_Ico_subset mem_nhdsWithin_Ici_iff_exists_Ico_subset

theorem nhdsWithin_Ici_basis_Ico [NoMaxOrder α] (a : α) :
    (𝓝[≥] a).HasBasis (fun u => a < u) (Ico a) :=
  ⟨fun _ => mem_nhdsWithin_Ici_iff_exists_Ico_subset⟩
#align nhds_within_Ici_basis_Ico nhdsWithin_Ici_basis_Ico

/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u]`
with `a < u`. -/
theorem mem_nhdsWithin_Ici_iff_exists_Icc_subset [NoMaxOrder α] [DenselyOrdered α] {a : α}
    {s : Set α} : s ∈ 𝓝[≥] a ↔ ∃ u, a < u ∧ Icc a u ⊆ s := by
  rw [mem_nhdsWithin_Ici_iff_exists_Ico_subset]
  constructor
  · rintro ⟨u, au, as⟩
    rcases exists_between au with ⟨v, hv⟩
    exact ⟨v, hv.1, fun x hx => as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩
  · rintro ⟨u, au, as⟩
    exact ⟨u, au, Subset.trans Ico_subset_Icc_self as⟩
#align mem_nhds_within_Ici_iff_exists_Icc_subset mem_nhdsWithin_Ici_iff_exists_Icc_subset

open List in
/-- The following statements are equivalent:

0. `s` is a neighborhood of `b` within `(-∞, b]`
1. `s` is a neighborhood of `b` within `[a, b]`
2. `s` is a neighborhood of `b` within `(a, b]`
3. `s` includes `(l, b]` for some `l ∈ [a, b)`
4. `s` includes `(l, b]` for some `l < b` -/
theorem TFAE_mem_nhdsWithin_Iic {a b : α} (h : a < b) (s : Set α) :
    TFAE [s ∈ 𝓝[≤] b,-- 0 : `s` is a neighborhood of `b` within `(-∞, b]`
      s ∈ 𝓝[Icc a b] b,-- 1 : `s` is a neighborhood of `b` within `[a, b]`
      s ∈ 𝓝[Ioc a b] b,-- 2 : `s` is a neighborhood of `b` within `(a, b]`
      ∃ l ∈ Ico a b, Ioc l b ⊆ s,-- 3 : `s` includes `(l, b]` for some `l ∈ [a, b)`
      ∃ l ∈ Iio b, Ioc l b ⊆ s] := by-- 4 : `s` includes `(l, b]` for some `l < b`
  simpa only [exists_prop, OrderDual.exists, dual_Ici, dual_Ioc, dual_Icc, dual_Ico] using
    TFAE_mem_nhdsWithin_Ici h.dual (ofDual ⁻¹' s)
#align tfae_mem_nhds_within_Iic TFAE_mem_nhdsWithin_Iic

theorem mem_nhdsWithin_Iic_iff_exists_mem_Ico_Ioc_subset {a l' : α} {s : Set α} (hl' : l' < a) :
    s ∈ 𝓝[≤] a ↔ ∃ l ∈ Ico l' a, Ioc l a ⊆ s :=
  (TFAE_mem_nhdsWithin_Iic hl' s).out 0 3 (by norm_num) (by norm_num)
#align mem_nhds_within_Iic_iff_exists_mem_Ico_Ioc_subset mem_nhdsWithin_Iic_iff_exists_mem_Ico_Ioc_subset

/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `(l, a]`
with `l < a`, provided `a` is not a bottom element. -/
theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset' {a l' : α} {s : Set α} (hl' : l' < a) :
    s ∈ 𝓝[≤] a ↔ ∃ l ∈ Iio a, Ioc l a ⊆ s :=
  (TFAE_mem_nhdsWithin_Iic hl' s).out 0 4 (by norm_num) (by norm_num)
#align mem_nhds_within_Iic_iff_exists_Ioc_subset' mem_nhdsWithin_Iic_iff_exists_Ioc_subset'

/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `(l, a]`
with `l < a`. -/
theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset [NoMinOrder α] {a : α} {s : Set α} :
    s ∈ 𝓝[≤] a ↔ ∃ l ∈ Iio a, Ioc l a ⊆ s :=
  let ⟨_, hl'⟩ := exists_lt a
  mem_nhdsWithin_Iic_iff_exists_Ioc_subset' hl'
#align mem_nhds_within_Iic_iff_exists_Ioc_subset mem_nhdsWithin_Iic_iff_exists_Ioc_subset

/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `[l, a]`
with `l < a`. -/
theorem mem_nhdsWithin_Iic_iff_exists_Icc_subset [NoMinOrder α] [DenselyOrdered α] {a : α}
    {s : Set α} : s ∈ 𝓝[≤] a ↔ ∃ l, l < a ∧ Icc l a ⊆ s :=
  calc s ∈ 𝓝[≤] a ↔ ofDual ⁻¹' s ∈ 𝓝[≥] (toDual a) := Iff.rfl
  _ ↔ ∃ u : α, toDual a < toDual u ∧ Icc (toDual a) (toDual u) ⊆ ofDual ⁻¹' s :=
    mem_nhdsWithin_Ici_iff_exists_Icc_subset
  _ ↔ ∃ l, l < a ∧ Icc l a ⊆ s := by simp only [dual_Icc]; rfl
#align mem_nhds_within_Iic_iff_exists_Icc_subset mem_nhdsWithin_Iic_iff_exists_Icc_subset

end OrderTopology

end LinearOrder

section LinearOrderedAddCommGroup

variable [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α]

variable {l : Filter β} {f g : β → α}

theorem nhds_eq_iInf_abs_sub (a : α) : 𝓝 a = ⨅ r > 0, 𝓟 { b | |a - b| < r } := by
  simp only [nhds_eq_order, abs_lt, setOf_and, ← inf_principal, iInf_inf_eq]
  refine (congr_arg₂ _ ?_ ?_).trans inf_comm
  · refine (Equiv.subLeft a).iInf_congr fun x => ?_; simp [Ioi]
  · refine (Equiv.subRight a).iInf_congr fun x => ?_; simp [Iio]
#align nhds_eq_infi_abs_sub nhds_eq_iInf_abs_sub

theorem orderTopology_of_nhds_abs {α : Type*} [TopologicalSpace α] [LinearOrderedAddCommGroup α]
    (h_nhds : ∀ a : α, 𝓝 a = ⨅ r > 0, 𝓟 { b | |a - b| < r }) : OrderTopology α := by
  refine' ⟨eq_of_nhds_eq_nhds fun a => _⟩
  rw [h_nhds]
  letI := Preorder.topology α; letI : OrderTopology α := ⟨rfl⟩
  exact (nhds_eq_iInf_abs_sub a).symm
#align order_topology_of_nhds_abs orderTopology_of_nhds_abs

theorem LinearOrderedAddCommGroup.tendsto_nhds {x : Filter β} {a : α} :
    Tendsto f x (𝓝 a) ↔ ∀ ε > (0 : α), ∀ᶠ b in x, |f b - a| < ε := by
  simp [nhds_eq_iInf_abs_sub, abs_sub_comm a]
#align linear_ordered_add_comm_group.tendsto_nhds LinearOrderedAddCommGroup.tendsto_nhds

theorem eventually_abs_sub_lt (a : α) {ε : α} (hε : 0 < ε) : ∀ᶠ x in 𝓝 a, |x - a| < ε :=
  (nhds_eq_iInf_abs_sub a).symm ▸
    mem_iInf_of_mem ε (mem_iInf_of_mem hε <| by simp only [abs_sub_comm, mem_principal_self])
#align eventually_abs_sub_lt eventually_abs_sub_lt

/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to `C`
and `g` tends to `atTop` then `f + g` tends to `atTop`. -/
theorem Filter.Tendsto.add_atTop {C : α} (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x + g x) l atTop := by
  nontriviality α
  obtain ⟨C', hC'⟩ : ∃ C', C' < C := exists_lt C
  refine' tendsto_atTop_add_left_of_le' _ C' _ hg
  exact (hf.eventually (lt_mem_nhds hC')).mono fun x => le_of_lt
#align filter.tendsto.add_at_top Filter.Tendsto.add_atTop

/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to `C`
and `g` tends to `atBot` then `f + g` tends to `atBot`. -/
theorem Filter.Tendsto.add_atBot {C : α} (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x + g x) l atBot :=
  Filter.Tendsto.add_atTop (α := αᵒᵈ) hf hg
#align filter.tendsto.add_at_bot Filter.Tendsto.add_atBot

/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to
`atTop` and `g` tends to `C` then `f + g` tends to `atTop`. -/
theorem Filter.Tendsto.atTop_add {C : α} (hf : Tendsto f l atTop) (hg : Tendsto g l (𝓝 C)) :
    Tendsto (fun x => f x + g x) l atTop := by
  conv in _ + _ => rw [add_comm]
  exact hg.add_atTop hf
#align filter.tendsto.at_top_add Filter.Tendsto.atTop_add

/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to
`atBot` and `g` tends to `C` then `f + g` tends to `atBot`. -/
theorem Filter.Tendsto.atBot_add {C : α} (hf : Tendsto f l atBot) (hg : Tendsto g l (𝓝 C)) :
    Tendsto (fun x => f x + g x) l atBot := by
  conv in _ + _ => rw [add_comm]
  exact hg.add_atBot hf
#align filter.tendsto.at_bot_add Filter.Tendsto.atBot_add

theorem nhds_basis_abs_sub_lt [NoMaxOrder α] (a : α) :
    (𝓝 a).HasBasis (fun ε : α => (0 : α) < ε) fun ε => { b | |b - a| < ε } := by
  simp only [nhds_eq_iInf_abs_sub, abs_sub_comm (a := a)]
  refine hasBasis_biInf_principal' (fun x hx y hy => ?_) (exists_gt _)
  exact ⟨min x y, lt_min hx hy, fun _ hz => hz.trans_le (min_le_left _ _),
    fun _ hz => hz.trans_le (min_le_right _ _)⟩
#align nhds_basis_abs_sub_lt nhds_basis_abs_sub_lt

theorem nhds_basis_Ioo_pos [NoMaxOrder α] (a : α) :
    (𝓝 a).HasBasis (fun ε : α => (0 : α) < ε) fun ε => Ioo (a - ε) (a + ε) := by
  convert nhds_basis_abs_sub_lt a
  simp only [Ioo, abs_lt, ← sub_lt_iff_lt_add, neg_lt_sub_iff_lt_add, sub_lt_comm]
#align nhds_basis_Ioo_pos nhds_basis_Ioo_pos

theorem nhds_basis_Icc_pos [NoMaxOrder α] [DenselyOrdered α] (a : α) :
    (𝓝 a).HasBasis ((0 : α) < ·) fun ε ↦ Icc (a - ε) (a + ε) :=
  (nhds_basis_Ioo_pos a).to_hasBasis
    (fun _ε ε₀ ↦ let ⟨δ, δ₀, δε⟩ := exists_between ε₀
      ⟨δ, δ₀, Icc_subset_Ioo (sub_lt_sub_left δε _) (add_lt_add_left δε _)⟩)
    (fun ε ε₀ ↦ ⟨ε, ε₀, Ioo_subset_Icc_self⟩)

variable (α)

theorem nhds_basis_zero_abs_sub_lt [NoMaxOrder α] :
    (𝓝 (0 : α)).HasBasis (fun ε : α => (0 : α) < ε) fun ε => { b | |b| < ε } := by
  simpa using nhds_basis_abs_sub_lt (0 : α)
#align nhds_basis_zero_abs_sub_lt nhds_basis_zero_abs_sub_lt

variable {α}

/-- If `a` is positive we can form a basis from only nonnegative `Set.Ioo` intervals -/
theorem nhds_basis_Ioo_pos_of_pos [NoMaxOrder α] {a : α} (ha : 0 < a) :
    (𝓝 a).HasBasis (fun ε : α => (0 : α) < ε ∧ ε ≤ a) fun ε => Ioo (a - ε) (a + ε) :=
  (nhds_basis_Ioo_pos a).restrict fun ε hε => ⟨min a ε, lt_min ha hε, min_le_left _ _,
    Ioo_subset_Ioo (sub_le_sub_left (min_le_right _ _) _) (add_le_add_left (min_le_right _ _) _)⟩
#align nhds_basis_Ioo_pos_of_pos nhds_basis_Ioo_pos_of_pos

end LinearOrderedAddCommGroup

@[deprecated image_neg]
theorem preimage_neg [AddGroup α] : preimage (Neg.neg : α → α) = image (Neg.neg : α → α) :=
  funext fun _ => image_neg.symm
#align preimage_neg preimage_neg

@[deprecated] -- use `Filter.map_neg` from `Mathlib.Order.Filter.Pointwise`
theorem Filter.map_neg_eq_comap_neg [AddGroup α] :
    map (Neg.neg : α → α) = comap (Neg.neg : α → α) :=
  funext fun _ => map_eq_comap_of_inverse (funext neg_neg) (funext neg_neg)
#align filter.map_neg_eq_comap_neg Filter.map_neg_eq_comap_neg

section OrderTopology

variable [TopologicalSpace α] [TopologicalSpace β] [LinearOrder α] [LinearOrder β] [OrderTopology α]
  [OrderTopology β]

theorem IsLUB.frequently_mem {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) :
    ∃ᶠ x in 𝓝[≤] a, x ∈ s := by
  rcases hs with ⟨a', ha'⟩
  intro h
  rcases (ha.1 ha').eq_or_lt with (rfl | ha'a)
  · exact h.self_of_nhdsWithin le_rfl ha'
  · rcases (mem_nhdsWithin_Iic_iff_exists_Ioc_subset' ha'a).1 h with ⟨b, hba, hb⟩
    rcases ha.exists_between hba with ⟨b', hb's, hb'⟩
    exact hb hb' hb's
#align is_lub.frequently_mem IsLUB.frequently_mem

theorem IsLUB.frequently_nhds_mem {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) :
    ∃ᶠ x in 𝓝 a, x ∈ s :=
  (ha.frequently_mem hs).filter_mono inf_le_left
#align is_lub.frequently_nhds_mem IsLUB.frequently_nhds_mem

theorem IsGLB.frequently_mem {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) :
    ∃ᶠ x in 𝓝[≥] a, x ∈ s :=
  IsLUB.frequently_mem (α := αᵒᵈ) ha hs
#align is_glb.frequently_mem IsGLB.frequently_mem

theorem IsGLB.frequently_nhds_mem {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) :
    ∃ᶠ x in 𝓝 a, x ∈ s :=
  (ha.frequently_mem hs).filter_mono inf_le_left
#align is_glb.frequently_nhds_mem IsGLB.frequently_nhds_mem

theorem IsLUB.mem_closure {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : a ∈ closure s :=
  (ha.frequently_nhds_mem hs).mem_closure
#align is_lub.mem_closure IsLUB.mem_closure

theorem IsGLB.mem_closure {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : a ∈ closure s :=
  (ha.frequently_nhds_mem hs).mem_closure
#align is_glb.mem_closure IsGLB.mem_closure

theorem IsLUB.nhdsWithin_neBot {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) :
    NeBot (𝓝[s] a) :=
  mem_closure_iff_nhdsWithin_neBot.1 (ha.mem_closure hs)
#align is_lub.nhds_within_ne_bot IsLUB.nhdsWithin_neBot

theorem IsGLB.nhdsWithin_neBot : ∀ {a : α} {s : Set α}, IsGLB s a → s.Nonempty → NeBot (𝓝[s] a) :=
  IsLUB.nhdsWithin_neBot (α := αᵒᵈ)
#align is_glb.nhds_within_ne_bot IsGLB.nhdsWithin_neBot

theorem isLUB_of_mem_nhds {s : Set α} {a : α} {f : Filter α} (hsa : a ∈ upperBounds s) (hsf : s ∈ f)
    [NeBot (f ⊓ 𝓝 a)] : IsLUB s a :=
  ⟨hsa, fun b hb =>
    not_lt.1 fun hba =>
      have : s ∩ { a | b < a } ∈ f ⊓ 𝓝 a := inter_mem_inf hsf (IsOpen.mem_nhds (isOpen_lt' _) hba)
      let ⟨_x, ⟨hxs, hxb⟩⟩ := Filter.nonempty_of_mem this
      have : b < b := lt_of_lt_of_le hxb <| hb hxs
      lt_irrefl b this⟩
#align is_lub_of_mem_nhds isLUB_of_mem_nhds

theorem isLUB_of_mem_closure {s : Set α} {a : α} (hsa : a ∈ upperBounds s) (hsf : a ∈ closure s) :
    IsLUB s a := by
  rw [mem_closure_iff_clusterPt, ClusterPt, inf_comm] at hsf
  exact isLUB_of_mem_nhds hsa (mem_principal_self s)
#align is_lub_of_mem_closure isLUB_of_mem_closure

theorem isGLB_of_mem_nhds :
    ∀ {s : Set α} {a : α} {f : Filter α}, a ∈ lowerBounds s → s ∈ f → NeBot (f ⊓ 𝓝 a) → IsGLB s a :=
  isLUB_of_mem_nhds (α := αᵒᵈ)
#align is_glb_of_mem_nhds isGLB_of_mem_nhds

theorem isGLB_of_mem_closure {s : Set α} {a : α} (hsa : a ∈ lowerBounds s) (hsf : a ∈ closure s) :
    IsGLB s a :=
  isLUB_of_mem_closure (α := αᵒᵈ) hsa hsf
#align is_glb_of_mem_closure isGLB_of_mem_closure

theorem IsLUB.mem_upperBounds_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ]
    {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a)
    (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : b ∈ upperBounds (f '' s) := by
  rintro _ ⟨x, hx, rfl⟩
  replace ha := ha.inter_Ici_of_mem hx
  haveI := ha.nhdsWithin_neBot ⟨x, hx, le_rfl⟩
  refine' ge_of_tendsto (hb.mono_left (nhdsWithin_mono _ (inter_subset_left s (Ici x)))) _
  exact mem_of_superset self_mem_nhdsWithin fun y hy => hf hx hy.1 hy.2
#align is_lub.mem_upper_bounds_of_tendsto IsLUB.mem_upperBounds_of_tendsto

-- For a version of this theorem in which the convergence considered on the domain `α` is as `x : α`
-- tends to infinity, rather than tending to a point `x` in `α`, see `isLUB_of_tendsto_atTop`
theorem IsLUB.isLUB_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ}
    {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) (hs : s.Nonempty)
    (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : IsLUB (f '' s) b :=
  haveI := ha.nhdsWithin_neBot hs
  ⟨ha.mem_upperBounds_of_tendsto hf hb, fun _b' hb' =>
    le_of_tendsto hb (mem_of_superset self_mem_nhdsWithin fun _ hx => hb' <| mem_image_of_mem _ hx)⟩
#align is_lub.is_lub_of_tendsto IsLUB.isLUB_of_tendsto

theorem IsGLB.mem_lowerBounds_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ]
    {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsGLB s a)
    (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : b ∈ lowerBounds (f '' s) :=
  IsLUB.mem_upperBounds_of_tendsto (α := αᵒᵈ) (γ := γᵒᵈ) hf.dual ha hb
#align is_glb.mem_lower_bounds_of_tendsto IsGLB.mem_lowerBounds_of_tendsto

-- For a version of this theorem in which the convergence considered on the domain `α` is as
-- `x : α` tends to negative infinity, rather than tending to a point `x` in `α`, see
-- `isGLB_of_tendsto_atBot`
theorem IsGLB.isGLB_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ}
    {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) :
    IsGLB s a → s.Nonempty → Tendsto f (𝓝[s] a) (𝓝 b) → IsGLB (f '' s) b :=
  IsLUB.isLUB_of_tendsto (α := αᵒᵈ) (γ := γᵒᵈ) hf.dual
#align is_glb.is_glb_of_tendsto IsGLB.isGLB_of_tendsto

theorem IsLUB.mem_lowerBounds_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ]
    {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsLUB s a)
    (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : b ∈ lowerBounds (f '' s) :=
  IsLUB.mem_upperBounds_of_tendsto (γ := γᵒᵈ) hf ha hb
#align is_lub.mem_lower_bounds_of_tendsto IsLUB.mem_lowerBounds_of_tendsto

theorem IsLUB.isGLB_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] :
    ∀ {f : α → γ} {s : Set α} {a : α} {b : γ},
      AntitoneOn f s → IsLUB s a → s.Nonempty → Tendsto f (𝓝[s] a) (𝓝 b) → IsGLB (f '' s) b :=
  IsLUB.isLUB_of_tendsto (γ := γᵒᵈ)
#align is_lub.is_glb_of_tendsto IsLUB.isGLB_of_tendsto

theorem IsGLB.mem_upperBounds_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ]
    {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsGLB s a)
    (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : b ∈ upperBounds (f '' s) :=
  IsGLB.mem_lowerBounds_of_tendsto (γ := γᵒᵈ) hf ha hb
#align is_glb.mem_upper_bounds_of_tendsto IsGLB.mem_upperBounds_of_tendsto

theorem IsGLB.isLUB_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] :
    ∀ {f : α → γ} {s : Set α} {a : α} {b : γ},
      AntitoneOn f s → IsGLB s a → s.Nonempty → Tendsto f (𝓝[s] a) (𝓝 b) → IsLUB (f '' s) b :=
  IsGLB.isGLB_of_tendsto (γ := γᵒᵈ)
#align is_glb.is_lub_of_tendsto IsGLB.isLUB_of_tendsto

theorem IsLUB.mem_of_isClosed {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty)
    (sc : IsClosed s) : a ∈ s :=
  sc.closure_subset <| ha.mem_closure hs
#align is_lub.mem_of_is_closed IsLUB.mem_of_isClosed

alias IsClosed.isLUB_mem := IsLUB.mem_of_isClosed
#align is_closed.is_lub_mem IsClosed.isLUB_mem

theorem IsGLB.mem_of_isClosed {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty)
    (sc : IsClosed s) : a ∈ s :=
  sc.closure_subset <| ha.mem_closure hs
#align is_glb.mem_of_is_closed IsGLB.mem_of_isClosed

alias IsClosed.isGLB_mem := IsGLB.mem_of_isClosed
#align is_closed.is_glb_mem IsClosed.isGLB_mem

/-!
### Existence of sequences tending to `sInf` or `sSup` of a given set
-/

theorem IsLUB.exists_seq_strictMono_tendsto_of_not_mem {t : Set α} {x : α}
    [IsCountablyGenerated (𝓝 x)] (htx : IsLUB t x) (not_mem : x ∉ t) (ht : t.Nonempty) :
    ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t := by
  obtain ⟨v, hvx, hvt⟩ := exists_seq_forall_of_frequently (htx.frequently_mem ht)
  replace hvx := hvx.mono_right nhdsWithin_le_nhds
  have hvx' : ∀ {n}, v n < x := (htx.1 (hvt _)).lt_of_ne (ne_of_mem_of_not_mem (hvt _) not_mem)
  have : ∀ k, ∀ᶠ l in atTop, v k < v l := fun k => hvx.eventually (lt_mem_nhds hvx')
  choose N hN hvN using fun k => ((eventually_gt_atTop k).and (this k)).exists
  refine ⟨fun k => v (N^[k] 0), strictMono_nat_of_lt_succ fun _ => ?_, fun _ => hvx',
    hvx.comp (strictMono_nat_of_lt_succ fun _ => ?_).tendsto_atTop, fun _ => hvt _⟩
  · rw [iterate_succ_apply']; exact hvN _
  · rw [iterate_succ_apply']; exact hN _
#align is_lub.exists_seq_strict_mono_tendsto_of_not_mem IsLUB.exists_seq_strictMono_tendsto_of_not_mem

theorem IsLUB.exists_seq_monotone_tendsto {t : Set α} {x : α} [IsCountablyGenerated (𝓝 x)]
    (htx : IsLUB t x) (ht : t.Nonempty) :
    ∃ u : ℕ → α, Monotone u ∧ (∀ n, u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t := by
  by_cases h : x ∈ t
  · exact ⟨fun _ => x, monotone_const, fun n => le_rfl, tendsto_const_nhds, fun _ => h⟩
  · rcases htx.exists_seq_strictMono_tendsto_of_not_mem h ht with ⟨u, hu⟩
    exact ⟨u, hu.1.monotone, fun n => (hu.2.1 n).le, hu.2.2⟩
#align is_lub.exists_seq_monotone_tendsto IsLUB.exists_seq_monotone_tendsto

theorem exists_seq_strictMono_tendsto' {α : Type*} [LinearOrder α] [TopologicalSpace α]
    [DenselyOrdered α] [OrderTopology α] [FirstCountableTopology α] {x y : α} (hy : y < x) :
    ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x) := by
  have hx : x ∉ Ioo y x := fun h => (lt_irrefl x h.2).elim
  have ht : Set.Nonempty (Ioo y x) := nonempty_Ioo.2 hy
  rcases (isLUB_Ioo hy).exists_seq_strictMono_tendsto_of_not_mem hx ht with ⟨u, hu⟩
  exact ⟨u, hu.1, hu.2.2.symm⟩
#align exists_seq_strict_mono_tendsto' exists_seq_strictMono_tendsto'

theorem exists_seq_strictMono_tendsto [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α]
    (x : α) : ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝 x) := by
  obtain ⟨y, hy⟩ : ∃ y, y < x := exists_lt x
  rcases exists_seq_strictMono_tendsto' hy with ⟨u, hu_mono, hu_mem, hux⟩
  exact ⟨u, hu_mono, fun n => (hu_mem n).2, hux⟩
#align exists_seq_strict_mono_tendsto exists_seq_strictMono_tendsto

theorem exists_seq_strictMono_tendsto_nhdsWithin [DenselyOrdered α] [NoMinOrder α]
    [FirstCountableTopology α] (x : α) :
    ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝[<] x) :=
  let ⟨u, hu, hx, h⟩ := exists_seq_strictMono_tendsto x
  ⟨u, hu, hx, tendsto_nhdsWithin_mono_right (range_subset_iff.2 hx) <| tendsto_nhdsWithin_range.2 h⟩
#align exists_seq_strict_mono_tendsto_nhds_within exists_seq_strictMono_tendsto_nhdsWithin

theorem exists_seq_tendsto_sSup {α : Type*} [ConditionallyCompleteLinearOrder α]
    [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {S : Set α} (hS : S.Nonempty)
    (hS' : BddAbove S) : ∃ u : ℕ → α, Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ n, u n ∈ S := by
  rcases (isLUB_csSup hS hS').exists_seq_monotone_tendsto hS with ⟨u, hu⟩
  exact ⟨u, hu.1, hu.2.2⟩
#align exists_seq_tendsto_Sup exists_seq_tendsto_sSup

theorem IsGLB.exists_seq_strictAnti_tendsto_of_not_mem {t : Set α} {x : α}
    [IsCountablyGenerated (𝓝 x)] (htx : IsGLB t x) (not_mem : x ∉ t) (ht : t.Nonempty) :
    ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, x < u n) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t :=
  IsLUB.exists_seq_strictMono_tendsto_of_not_mem (α := αᵒᵈ) htx not_mem ht
#align is_glb.exists_seq_strict_anti_tendsto_of_not_mem IsGLB.exists_seq_strictAnti_tendsto_of_not_mem

theorem IsGLB.exists_seq_antitone_tendsto {t : Set α} {x : α} [IsCountablyGenerated (𝓝 x)]
    (htx : IsGLB t x) (ht : t.Nonempty) :
    ∃ u : ℕ → α, Antitone u ∧ (∀ n, x ≤ u n) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t :=
  IsLUB.exists_seq_monotone_tendsto (α := αᵒᵈ) htx ht
#align is_glb.exists_seq_antitone_tendsto IsGLB.exists_seq_antitone_tendsto

theorem exists_seq_strictAnti_tendsto' [DenselyOrdered α] [FirstCountableTopology α] {x y : α}
    (hy : x < y) : ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, u n ∈ Ioo x y) ∧ Tendsto u atTop (𝓝 x) := by
  simpa only [dual_Ioo]
    using exists_seq_strictMono_tendsto' (α := αᵒᵈ) (OrderDual.toDual_lt_toDual.2 hy)
#align exists_seq_strict_anti_tendsto' exists_seq_strictAnti_tendsto'

theorem exists_seq_strictAnti_tendsto [DenselyOrdered α] [NoMaxOrder α] [FirstCountableTopology α]
    (x : α) : ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, x < u n) ∧ Tendsto u atTop (𝓝 x) :=
  exists_seq_strictMono_tendsto (α := αᵒᵈ) x
#align exists_seq_strict_anti_tendsto exists_seq_strictAnti_tendsto

theorem exists_seq_strictAnti_tendsto_nhdsWithin [DenselyOrdered α] [NoMaxOrder α]
    [FirstCountableTopology α] (x : α) :
    ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, x < u n) ∧ Tendsto u atTop (𝓝[>] x) :=
  exists_seq_strictMono_tendsto_nhdsWithin (α := αᵒᵈ) _
#align exists_seq_strict_anti_tendsto_nhds_within exists_seq_strictAnti_tendsto_nhdsWithin

theorem exists_seq_strictAnti_strictMono_tendsto [DenselyOrdered α] [FirstCountableTopology α]
    {x y : α} (h : x < y) :
    ∃ u v : ℕ → α, StrictAnti u ∧ StrictMono v ∧ (∀ k, u k ∈ Ioo x y) ∧ (∀ l, v l ∈ Ioo x y) ∧
      (∀ k l, u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y) := by
  rcases exists_seq_strictAnti_tendsto' h with ⟨u, hu_anti, hu_mem, hux⟩
  rcases exists_seq_strictMono_tendsto' (hu_mem 0).2 with ⟨v, hv_mono, hv_mem, hvy⟩
  exact
    ⟨u, v, hu_anti, hv_mono, hu_mem, fun l => ⟨(hu_mem 0).1.trans (hv_mem l).1, (hv_mem l).2⟩,
      fun k l => (hu_anti.antitone (zero_le k)).trans_lt (hv_mem l).1, hux, hvy⟩
#align exists_seq_strict_anti_strict_mono_tendsto exists_seq_strictAnti_strictMono_tendsto

theorem exists_seq_tendsto_sInf {α : Type*} [ConditionallyCompleteLinearOrder α]
    [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {S : Set α} (hS : S.Nonempty)
    (hS' : BddBelow S) : ∃ u : ℕ → α, Antitone u ∧ Tendsto u atTop (𝓝 (sInf S)) ∧ ∀ n, u n ∈ S :=
  exists_seq_tendsto_sSup (α := αᵒᵈ) hS hS'
#align exists_seq_tendsto_Inf exists_seq_tendsto_sInf

end OrderTopology

section DenselyOrdered

variable [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α}
  {s : Set α}

/-- The closure of the interval `(a, +∞)` is the closed interval `[a, +∞)`, unless `a` is a top
element. -/
theorem closure_Ioi' {a : α} (h : (Ioi a).Nonempty) : closure (Ioi a) = Ici a := by
  apply Subset.antisymm
  · exact closure_minimal Ioi_subset_Ici_self isClosed_Ici
  · rw [← diff_subset_closure_iff, Ici_diff_Ioi_same, singleton_subset_iff]
    exact isGLB_Ioi.mem_closure h
#align closure_Ioi' closure_Ioi'

/-- The closure of the interval `(a, +∞)` is the closed interval `[a, +∞)`. -/
@[simp]
theorem closure_Ioi (a : α) [NoMaxOrder α] : closure (Ioi a) = Ici a :=
  closure_Ioi' nonempty_Ioi
#align closure_Ioi closure_Ioi

/-- The closure of the interval `(-∞, a)` is the closed interval `(-∞, a]`, unless `a` is a bottom
element. -/
theorem closure_Iio' (h : (Iio a).Nonempty) : closure (Iio a) = Iic a :=
  closure_Ioi' (α := αᵒᵈ) h
#align closure_Iio' closure_Iio'

/-- The closure of the interval `(-∞, a)` is the interval `(-∞, a]`. -/
@[simp]
theorem closure_Iio (a : α) [NoMinOrder α] : closure (Iio a) = Iic a :=
  closure_Iio' nonempty_Iio
#align closure_Iio closure_Iio

/-- The closure of the open interval `(a, b)` is the closed interval `[a, b]`. -/
@[simp]
theorem closure_Ioo {a b : α} (hab : a ≠ b) : closure (Ioo a b) = Icc a b := by
  apply Subset.antisymm
  · exact closure_minimal Ioo_subset_Icc_self isClosed_Icc
  · cases' hab.lt_or_lt with hab hab
    · rw [← diff_subset_closure_iff, Icc_diff_Ioo_same hab.le]
      have hab' : (Ioo a b).Nonempty := nonempty_Ioo.2 hab
      simp only [insert_subset_iff, singleton_subset_iff]
      exact ⟨(isGLB_Ioo hab).mem_closure hab', (isLUB_Ioo hab).mem_closure hab'⟩
    · rw [Icc_eq_empty_of_lt hab]
      exact empty_subset _
#align closure_Ioo closure_Ioo

/-- The closure of the interval `(a, b]` is the closed interval `[a, b]`. -/
@[simp]
theorem closure_Ioc {a b : α} (hab : a ≠ b) : closure (Ioc a b) = Icc a b := by
  apply Subset.antisymm
  · exact closure_minimal Ioc_subset_Icc_self isClosed_Icc
  · apply Subset.trans _ (closure_mono Ioo_subset_Ioc_self)
    rw [closure_Ioo hab]
#align closure_Ioc closure_Ioc

/-- The closure of the interval `[a, b)` is the closed interval `[a, b]`. -/
@[simp]
theorem closure_Ico {a b : α} (hab : a ≠ b) : closure (Ico a b) = Icc a b := by
  apply Subset.antisymm
  · exact closure_minimal Ico_subset_Icc_self isClosed_Icc
  · apply Subset.trans _ (closure_mono Ioo_subset_Ico_self)
    rw [closure_Ioo hab]
#align closure_Ico closure_Ico

@[simp]
theorem interior_Ici' {a : α} (ha : (Iio a).Nonempty) : interior (Ici a) = Ioi a := by
  rw [← compl_Iio, interior_compl, closure_Iio' ha, compl_Iic]
#align interior_Ici' interior_Ici'

theorem interior_Ici [NoMinOrder α] {a : α} : interior (Ici a) = Ioi a :=
  interior_Ici' nonempty_Iio
#align interior_Ici interior_Ici

@[simp]
theorem interior_Iic' {a : α} (ha : (Ioi a).Nonempty) : interior (Iic a) = Iio a :=
  interior_Ici' (α := αᵒᵈ) ha
#align interior_Iic' interior_Iic'

theorem interior_Iic [NoMaxOrder α] {a : α} : interior (Iic a) = Iio a :=
  interior_Iic' nonempty_Ioi
#align interior_Iic interior_Iic

@[simp]
theorem interior_Icc [NoMinOrder α] [NoMaxOrder α] {a b : α} : interior (Icc a b) = Ioo a b := by
  rw [← Ici_inter_Iic, interior_inter, interior_Ici, interior_Iic, Ioi_inter_Iio]
#align interior_Icc interior_Icc

@[simp]
theorem interior_Ico [NoMinOrder α] {a b : α} : interior (Ico a b) = Ioo a b := by
  rw [← Ici_inter_Iio, interior_inter, interior_Ici, interior_Iio, Ioi_inter_Iio]
#align interior_Ico interior_Ico

@[simp]
theorem interior_Ioc [NoMaxOrder α] {a b : α} : interior (Ioc a b) = Ioo a b := by
  rw [← Ioi_inter_Iic, interior_inter, interior_Ioi, interior_Iic, Ioi_inter_Iio]
#align interior_Ioc interior_Ioc

theorem closure_interior_Icc {a b : α} (h : a ≠ b) : closure (interior (Icc a b)) = Icc a b :=
  (closure_minimal interior_subset isClosed_Icc).antisymm <|
    calc
      Icc a b = closure (Ioo a b) := (closure_Ioo h).symm
      _ ⊆ closure (interior (Icc a b)) :=
        closure_mono (interior_maximal Ioo_subset_Icc_self isOpen_Ioo)
#align closure_interior_Icc closure_interior_Icc

theorem Ioc_subset_closure_interior (a b : α) : Ioc a b ⊆ closure (interior (Ioc a b)) := by
  rcases eq_or_ne a b with (rfl | h)
  · simp
  · calc
      Ioc a b ⊆ Icc a b := Ioc_subset_Icc_self
      _ = closure (Ioo a b) := (closure_Ioo h).symm
      _ ⊆ closure (interior (Ioc a b)) :=
        closure_mono (interior_maximal Ioo_subset_Ioc_self isOpen_Ioo)
#align Ioc_subset_closure_interior Ioc_subset_closure_interior

theorem Ico_subset_closure_interior (a b : α) : Ico a b ⊆ closure (interior (Ico a b)) := by
  simpa only [dual_Ioc] using Ioc_subset_closure_interior (OrderDual.toDual b) (OrderDual.toDual a)
#align Ico_subset_closure_interior Ico_subset_closure_interior

@[simp]
theorem frontier_Ici' {a : α} (ha : (Iio a).Nonempty) : frontier (Ici a) = {a} := by
  simp [frontier, ha]
#align frontier_Ici' frontier_Ici'

theorem frontier_Ici [NoMinOrder α] {a : α} : frontier (Ici a) = {a} :=
  frontier_Ici' nonempty_Iio
#align frontier_Ici frontier_Ici

@[simp]
theorem frontier_Iic' {a : α} (ha : (Ioi a).Nonempty) : frontier (Iic a) = {a} := by
  simp [frontier, ha]
#align frontier_Iic' frontier_Iic'

theorem frontier_Iic [NoMaxOrder α] {a : α} : frontier (Iic a) = {a} :=
  frontier_Iic' nonempty_Ioi
#align frontier_Iic frontier_Iic

@[simp]
theorem frontier_Ioi' {a : α} (ha : (Ioi a).Nonempty) : frontier (Ioi a) = {a} := by
  simp [frontier, closure_Ioi' ha, Iic_diff_Iio, Icc_self]
#align frontier_Ioi' frontier_Ioi'

theorem frontier_Ioi [NoMaxOrder α] {a : α} : frontier (Ioi a) = {a} :=
  frontier_Ioi' nonempty_Ioi
#align frontier_Ioi frontier_Ioi

@[simp]
theorem frontier_Iio' {a : α} (ha : (Iio a).Nonempty) : frontier (Iio a) = {a} := by
  simp [frontier, closure_Iio' ha, Iic_diff_Iio, Icc_self]
#align frontier_Iio' frontier_Iio'

theorem frontier_Iio [NoMinOrder α] {a : α} : frontier (Iio a) = {a} :=
  frontier_Iio' nonempty_Iio
#align frontier_Iio frontier_Iio

@[simp]
theorem frontier_Icc [NoMinOrder α] [NoMaxOrder α] {a b : α} (h : a ≤ b) :
    frontier (Icc a b) = {a, b} := by simp [frontier, h, Icc_diff_Ioo_same]
#align frontier_Icc frontier_Icc

@[simp]
theorem frontier_Ioo {a b : α} (h : a < b) : frontier (Ioo a b) = {a, b} := by
  rw [frontier, closure_Ioo h.ne, interior_Ioo, Icc_diff_Ioo_same h.le]
#align frontier_Ioo frontier_Ioo

@[simp]
theorem frontier_Ico [NoMinOrder α] {a b : α} (h : a < b) : frontier (Ico a b) = {a, b} := by
  rw [frontier, closure_Ico h.ne, interior_Ico, Icc_diff_Ioo_same h.le]
#align frontier_Ico frontier_Ico

@[simp]
theorem frontier_Ioc [NoMaxOrder α] {a b : α} (h : a < b) : frontier (Ioc a b) = {a, b} := by
  rw [frontier, closure_Ioc h.ne, interior_Ioc, Icc_diff_Ioo_same h.le]
#align frontier_Ioc frontier_Ioc

theorem nhdsWithin_Ioi_neBot' {a b : α} (H₁ : (Ioi a).Nonempty) (H₂ : a ≤ b) :
    NeBot (𝓝[Ioi a] b) :=
  mem_closure_iff_nhdsWithin_neBot.1 <| by rwa [closure_Ioi' H₁]
#align nhds_within_Ioi_ne_bot' nhdsWithin_Ioi_neBot'

theorem nhdsWithin_Ioi_neBot [NoMaxOrder α] {a b : α} (H : a ≤ b) : NeBot (𝓝[Ioi a] b) :=
  nhdsWithin_Ioi_neBot' nonempty_Ioi H
#align nhds_within_Ioi_ne_bot nhdsWithin_Ioi_neBot

theorem nhdsWithin_Ioi_self_neBot' {a : α} (H : (Ioi a).Nonempty) : NeBot (𝓝[>] a) :=
  nhdsWithin_Ioi_neBot' H (le_refl a)
#align nhds_within_Ioi_self_ne_bot' nhdsWithin_Ioi_self_neBot'

instance nhdsWithin_Ioi_self_neBot [NoMaxOrder α] (a : α) : NeBot (𝓝[>] a) :=
  nhdsWithin_Ioi_neBot (le_refl a)
#align nhds_within_Ioi_self_ne_bot nhdsWithin_Ioi_self_neBot

theorem Filter.Eventually.exists_gt [NoMaxOrder α] {a : α} {p : α → Prop} (h : ∀ᶠ x in 𝓝 a, p x) :
    ∃ b > a, p b := by
  simpa only [exists_prop, gt_iff_lt, and_comm] using
    ((h.filter_mono (@nhdsWithin_le_nhds _ _ a (Ioi a))).and self_mem_nhdsWithin).exists
#align filter.eventually.exists_gt Filter.Eventually.exists_gt

theorem nhdsWithin_Iio_neBot' {b c : α} (H₁ : (Iio c).Nonempty) (H₂ : b ≤ c) :
    NeBot (𝓝[Iio c] b) :=
  mem_closure_iff_nhdsWithin_neBot.1 <| by rwa [closure_Iio' H₁]
#align nhds_within_Iio_ne_bot' nhdsWithin_Iio_neBot'

theorem nhdsWithin_Iio_neBot [NoMinOrder α] {a b : α} (H : a ≤ b) : NeBot (𝓝[Iio b] a) :=
  nhdsWithin_Iio_neBot' nonempty_Iio H
#align nhds_within_Iio_ne_bot nhdsWithin_Iio_neBot

theorem nhdsWithin_Iio_self_neBot' {b : α} (H : (Iio b).Nonempty) : NeBot (𝓝[<] b) :=
  nhdsWithin_Iio_neBot' H (le_refl b)
#align nhds_within_Iio_self_ne_bot' nhdsWithin_Iio_self_neBot'

instance nhdsWithin_Iio_self_neBot [NoMinOrder α] (a : α) : NeBot (𝓝[<] a) :=
  nhdsWithin_Iio_neBot (le_refl a)
#align nhds_within_Iio_self_ne_bot nhdsWithin_Iio_self_neBot

theorem Filter.Eventually.exists_lt [NoMinOrder α] {a : α} {p : α → Prop} (h : ∀ᶠ x in 𝓝 a, p x) :
    ∃ b < a, p b :=
  Filter.Eventually.exists_gt (α := αᵒᵈ) h
#align filter.eventually.exists_lt Filter.Eventually.exists_lt

theorem right_nhdsWithin_Ico_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ico a b] b) :=
  (isLUB_Ico H).nhdsWithin_neBot (nonempty_Ico.2 H)
#align right_nhds_within_Ico_ne_bot right_nhdsWithin_Ico_neBot

theorem left_nhdsWithin_Ioc_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ioc a b] a) :=
  (isGLB_Ioc H).nhdsWithin_neBot (nonempty_Ioc.2 H)
#align left_nhds_within_Ioc_ne_bot left_nhdsWithin_Ioc_neBot

theorem left_nhdsWithin_Ioo_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ioo a b] a) :=
  (isGLB_Ioo H).nhdsWithin_neBot (nonempty_Ioo.2 H)
#align left_nhds_within_Ioo_ne_bot left_nhdsWithin_Ioo_neBot

theorem right_nhdsWithin_Ioo_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ioo a b] b) :=
  (isLUB_Ioo H).nhdsWithin_neBot (nonempty_Ioo.2 H)
#align right_nhds_within_Ioo_ne_bot right_nhdsWithin_Ioo_neBot

theorem comap_coe_nhdsWithin_Iio_of_Ioo_subset (hb : s ⊆ Iio b)
    (hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s) : comap ((↑) : s → α) (𝓝[<] b) = atTop := by
  nontriviality
  haveI : Nonempty s := nontrivial_iff_nonempty.1 ‹_›
  rcases hs (nonempty_subtype.1 ‹_›) with ⟨a, h, hs⟩
  ext u; constructor
  · rintro ⟨t, ht, hts⟩
    obtain ⟨x, ⟨hxa : a ≤ x, hxb : x < b⟩, hxt : Ioo x b ⊆ t⟩ :=
      (mem_nhdsWithin_Iio_iff_exists_mem_Ico_Ioo_subset h).mp ht
    obtain ⟨y, hxy, hyb⟩ := exists_between hxb
    refine' mem_of_superset (mem_atTop ⟨y, hs ⟨hxa.trans_lt hxy, hyb⟩⟩) _
    rintro ⟨z, hzs⟩ (hyz : y ≤ z)
    exact hts (hxt ⟨hxy.trans_le hyz, hb hzs⟩)
  · intro hu
    obtain ⟨x : s, hx : ∀ z, x ≤ z → z ∈ u⟩ := mem_atTop_sets.1 hu
    exact ⟨Ioo x b, Ioo_mem_nhdsWithin_Iio' (hb x.2), fun z hz => hx _ hz.1.le⟩
#align comap_coe_nhds_within_Iio_of_Ioo_subset comap_coe_nhdsWithin_Iio_of_Ioo_subset

theorem comap_coe_nhdsWithin_Ioi_of_Ioo_subset (ha : s ⊆ Ioi a)
    (hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s) : comap ((↑) : s → α) (𝓝[>] a) = atBot :=
  comap_coe_nhdsWithin_Iio_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from ha) fun h => by
    simpa only [OrderDual.exists, dual_Ioo] using hs h
#align comap_coe_nhds_within_Ioi_of_Ioo_subset comap_coe_nhdsWithin_Ioi_of_Ioo_subset

theorem map_coe_atTop_of_Ioo_subset (hb : s ⊆ Iio b) (hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s) :
    map ((↑) : s → α) atTop = 𝓝[<] b := by
  rcases eq_empty_or_nonempty (Iio b) with (hb' | ⟨a, ha⟩)
  · have : IsEmpty s := ⟨fun x => hb'.subset (hb x.2)⟩
    rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty]
  · rw [← comap_coe_nhdsWithin_Iio_of_Ioo_subset hb fun _ => hs a ha, map_comap_of_mem]
    rw [Subtype.range_val]
    exact (mem_nhdsWithin_Iio_iff_exists_Ioo_subset' ha).2 (hs a ha)
#align map_coe_at_top_of_Ioo_subset map_coe_atTop_of_Ioo_subset

theorem map_coe_atBot_of_Ioo_subset (ha : s ⊆ Ioi a) (hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s) :
    map ((↑) : s → α) atBot = 𝓝[>] a := by
  -- the elaborator gets stuck without `(... : _)`
  refine' (map_coe_atTop_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from ha)
    fun b' hb' => _ : _)
  simpa only [OrderDual.exists, dual_Ioo] using hs b' hb'
#align map_coe_at_bot_of_Ioo_subset map_coe_atBot_of_Ioo_subset

/-- The `atTop` filter for an open interval `Ioo a b` comes from the left-neighbourhoods filter at
the right endpoint in the ambient order. -/
theorem comap_coe_Ioo_nhdsWithin_Iio (a b : α) : comap ((↑) : Ioo a b → α) (𝓝[<] b) = atTop :=
  comap_coe_nhdsWithin_Iio_of_Ioo_subset Ioo_subset_Iio_self fun h =>
    ⟨a, nonempty_Ioo.1 h, Subset.refl _⟩
#align comap_coe_Ioo_nhds_within_Iio comap_coe_Ioo_nhdsWithin_Iio

/-- The `atBot` filter for an open interval `Ioo a b` comes from the right-neighbourhoods filter at
the left endpoint in the ambient order. -/
theorem comap_coe_Ioo_nhdsWithin_Ioi (a b : α) : comap ((↑) : Ioo a b → α) (𝓝[>] a) = atBot :=
  comap_coe_nhdsWithin_Ioi_of_Ioo_subset Ioo_subset_Ioi_self fun h =>
    ⟨b, nonempty_Ioo.1 h, Subset.refl _⟩
#align comap_coe_Ioo_nhds_within_Ioi comap_coe_Ioo_nhdsWithin_Ioi

theorem comap_coe_Ioi_nhdsWithin_Ioi (a : α) : comap ((↑) : Ioi a → α) (𝓝[>] a) = atBot :=
  comap_coe_nhdsWithin_Ioi_of_Ioo_subset (Subset.refl _) fun ⟨x, hx⟩ => ⟨x, hx, Ioo_subset_Ioi_self⟩
#align comap_coe_Ioi_nhds_within_Ioi comap_coe_Ioi_nhdsWithin_Ioi

theorem comap_coe_Iio_nhdsWithin_Iio (a : α) : comap ((↑) : Iio a → α) (𝓝[<] a) = atTop :=
  comap_coe_Ioi_nhdsWithin_Ioi (α := αᵒᵈ) a
#align comap_coe_Iio_nhds_within_Iio comap_coe_Iio_nhdsWithin_Iio

@[simp]
theorem map_coe_Ioo_atTop {a b : α} (h : a < b) : map ((↑) : Ioo a b → α) atTop = 𝓝[<] b :=
  map_coe_atTop_of_Ioo_subset Ioo_subset_Iio_self fun _ _ => ⟨_, h, Subset.refl _⟩
#align map_coe_Ioo_at_top map_coe_Ioo_atTop

@[simp]
theorem map_coe_Ioo_atBot {a b : α} (h : a < b) : map ((↑) : Ioo a b → α) atBot = 𝓝[>] a :=
  map_coe_atBot_of_Ioo_subset Ioo_subset_Ioi_self fun _ _ => ⟨_, h, Subset.refl _⟩
#align map_coe_Ioo_at_bot map_coe_Ioo_atBot

@[simp]
theorem map_coe_Ioi_atBot (a : α) : map ((↑) : Ioi a → α) atBot = 𝓝[>] a :=
  map_coe_atBot_of_Ioo_subset (Subset.refl _) fun b hb => ⟨b, hb, Ioo_subset_Ioi_self⟩
#align map_coe_Ioi_at_bot map_coe_Ioi_atBot

@[simp]
theorem map_coe_Iio_atTop (a : α) : map ((↑) : Iio a → α) atTop = 𝓝[<] a :=
  map_coe_Ioi_atBot (α := αᵒᵈ) _
#align map_coe_Iio_at_top map_coe_Iio_atTop

variable {l : Filter β} {f : α → β}

@[simp]
theorem tendsto_comp_coe_Ioo_atTop (h : a < b) :
    Tendsto (fun x : Ioo a b => f x) atTop l ↔ Tendsto f (𝓝[<] b) l := by
  rw [← map_coe_Ioo_atTop h, tendsto_map'_iff]; rfl
#align tendsto_comp_coe_Ioo_at_top tendsto_comp_coe_Ioo_atTop

@[simp]
theorem tendsto_comp_coe_Ioo_atBot (h : a < b) :
    Tendsto (fun x : Ioo a b => f x) atBot l ↔ Tendsto f (𝓝[>] a) l := by
  rw [← map_coe_Ioo_atBot h, tendsto_map'_iff]; rfl
#align tendsto_comp_coe_Ioo_at_bot tendsto_comp_coe_Ioo_atBot

-- porting note: todo: `simpNF` claims that `simp` can't use this lemma to simplify LHS but it can
@[simp, nolint simpNF]
theorem tendsto_comp_coe_Ioi_atBot :
    Tendsto (fun x : Ioi a => f x) atBot l ↔ Tendsto f (𝓝[>] a) l := by
  rw [← map_coe_Ioi_atBot, tendsto_map'_iff]; rfl
#align tendsto_comp_coe_Ioi_at_bot tendsto_comp_coe_Ioi_atBot

-- porting note: todo: `simpNF` claims that `simp` can't use this lemma to simplify LHS but it can
@[simp, nolint simpNF]
theorem tendsto_comp_coe_Iio_atTop :
    Tendsto (fun x : Iio a => f x) atTop l ↔ Tendsto f (𝓝[<] a) l := by
  rw [← map_coe_Iio_atTop, tendsto_map'_iff]; rfl
#align tendsto_comp_coe_Iio_at_top tendsto_comp_coe_Iio_atTop

@[simp]
theorem tendsto_Ioo_atTop {f : β → Ioo a b} :
    Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l (𝓝[<] b) := by
  rw [← comap_coe_Ioo_nhdsWithin_Iio, tendsto_comap_iff]; rfl
#align tendsto_Ioo_at_top tendsto_Ioo_atTop

@[simp]
theorem tendsto_Ioo_atBot {f : β → Ioo a b} :
    Tendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l (𝓝[>] a) := by
  rw [← comap_coe_Ioo_nhdsWithin_Ioi, tendsto_comap_iff]; rfl
#align tendsto_Ioo_at_bot tendsto_Ioo_atBot

@[simp]
theorem tendsto_Ioi_atBot {f : β → Ioi a} :
    Tendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l (𝓝[>] a) := by
  rw [← comap_coe_Ioi_nhdsWithin_Ioi, tendsto_comap_iff]; rfl
#align tendsto_Ioi_at_bot tendsto_Ioi_atBot

@[simp]
theorem tendsto_Iio_atTop {f : β → Iio a} :
    Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l (𝓝[<] a) := by
  rw [← comap_coe_Iio_nhdsWithin_Iio, tendsto_comap_iff]; rfl
#align tendsto_Iio_at_top tendsto_Iio_atTop

instance (x : α) [Nontrivial α] : NeBot (𝓝[≠] x) := by
  refine forall_mem_nonempty_iff_neBot.1 fun s hs => ?_
  obtain ⟨u, u_open, xu, us⟩ : ∃ u : Set α, IsOpen u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ s := mem_nhdsWithin.1 hs
  obtain ⟨a, b, a_lt_b, hab⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ u := u_open.exists_Ioo_subset ⟨x, xu⟩
  obtain ⟨y, hy⟩ : ∃ y, a < y ∧ y < b := exists_between a_lt_b
  rcases ne_or_eq x y with (xy | rfl)
  · exact ⟨y, us ⟨hab hy, xy.symm⟩⟩
  obtain ⟨z, hz⟩ : ∃ z, a < z ∧ z < x := exists_between hy.1
  exact ⟨z, us ⟨hab ⟨hz.1, hz.2.trans hy.2⟩, hz.2.ne⟩⟩

/-- Let `s` be a dense set in a nontrivial dense linear order `α`. If `s` is a
separable space (e.g., if `α` has a second countable topology), then there exists a countable
dense subset `t ⊆ s` such that `t` does not contain bottom/top elements of `α`. -/
theorem Dense.exists_countable_dense_subset_no_bot_top [Nontrivial α] {s : Set α} [SeparableSpace s]
    (hs : Dense s) :
    ∃ t, t ⊆ s ∧ t.Countable ∧ Dense t ∧ (∀ x, IsBot x → x ∉ t) ∧ ∀ x, IsTop x → x ∉ t := by
  rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩
  refine' ⟨t \ ({ x | IsBot x } ∪ { x | IsTop x }), _, _, _, fun x hx => _, fun x hx => _⟩
  · exact (diff_subset _ _).trans hts
  · exact htc.mono (diff_subset _ _)
  · exact htd.diff_finite ((subsingleton_isBot α).finite.union (subsingleton_isTop α).finite)
  · simp [hx]
  · simp [hx]
#align dense.exists_countable_dense_subset_no_bot_top Dense.exists_countable_dense_subset_no_bot_top

variable (α)

/-- If `α` is a nontrivial separable dense linear order, then there exists a
countable dense set `s : Set α` that contains neither top nor bottom elements of `α`.
For a dense set containing both bot and top elements, see
`exists_countable_dense_bot_top`. -/
theorem exists_countable_dense_no_bot_top [SeparableSpace α] [Nontrivial α] :
    ∃ s : Set α, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∉ s) ∧ ∀ x, IsTop x → x ∉ s := by
  simpa using dense_univ.exists_countable_dense_subset_no_bot_top
#align exists_countable_dense_no_bot_top exists_countable_dense_no_bot_top

end DenselyOrdered

section ConditionallyCompleteLinearOrder

variable [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α]
  [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] [Nonempty γ]

/-- A monotone function continuous at the supremum of a nonempty set sends this supremum to
the supremum of the image of this set. -/
theorem Monotone.map_sSup_of_continuousAt' {f : α → β} {A : Set α} (Cf : ContinuousAt f (sSup A))
    (Mf : Monotone f) (A_nonemp : A.Nonempty) (A_bdd : BddAbove A := by bddDefault) :
    f (sSup A) = sSup (f '' A) :=
  --This is a particular case of the more general `IsLUB.isLUB_of_tendsto`
  .symm <| ((isLUB_csSup A_nonemp A_bdd).isLUB_of_tendsto (Mf.monotoneOn _) A_nonemp <|
    Cf.mono_left inf_le_left).csSup_eq (A_nonemp.image f)
#align monotone.map_Sup_of_continuous_at' Monotone.map_sSup_of_continuousAt'

/-- A monotone function continuous at the indexed supremum over a nonempty `Sort` sends this indexed
supremum to the indexed supremum of the composition. -/
theorem Monotone.map_iSup_of_continuousAt' {ι : Sort*} [Nonempty ι] {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iSup g)) (Mf : Monotone f)
    (bdd : BddAbove (range g) := by bddDefault) : f (⨆ i, g i) = ⨆ i, f (g i) := by
  rw [iSup, Monotone.map_sSup_of_continuousAt' Cf Mf (range_nonempty g) bdd, ← range_comp, iSup]
  rfl
#align monotone.map_supr_of_continuous_at' Monotone.map_iSup_of_continuousAt'

/-- A monotone function continuous at the infimum of a nonempty set sends this infimum to
the infimum of the image of this set. -/
theorem Monotone.map_sInf_of_continuousAt' {f : α → β} {A : Set α} (Cf : ContinuousAt f (sInf A))
    (Mf : Monotone f) (A_nonemp : A.Nonempty) (A_bdd : BddBelow A := by bddDefault) :
    f (sInf A) = sInf (f '' A) :=
  Monotone.map_sSup_of_continuousAt' (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual A_nonemp A_bdd
#align monotone.map_Inf_of_continuous_at' Monotone.map_sInf_of_continuousAt'

/-- A monotone function continuous at the indexed infimum over a nonempty `Sort` sends this indexed
infimum to the indexed infimum of the composition. -/
theorem Monotone.map_iInf_of_continuousAt' {ι : Sort*} [Nonempty ι] {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iInf g)) (Mf : Monotone f)
    (bdd : BddBelow (range g) := by bddDefault) : f (⨅ i, g i) = ⨅ i, f (g i) := by
  rw [iInf, Monotone.map_sInf_of_continuousAt' Cf Mf (range_nonempty g) bdd, ← range_comp, iInf]
  rfl
#align monotone.map_infi_of_continuous_at' Monotone.map_iInf_of_continuousAt'

/-- An antitone function continuous at the infimum of a nonempty set sends this infimum to
the supremum of the image of this set. -/
theorem Antitone.map_sInf_of_continuousAt' {f : α → β} {A : Set α} (Cf : ContinuousAt f (sInf A))
    (Af : Antitone f) (A_nonemp : A.Nonempty) (A_bdd : BddBelow A := by bddDefault) :
    f (sInf A) = sSup (f '' A) :=
  Monotone.map_sInf_of_continuousAt' (β := βᵒᵈ) Cf Af.dual_right A_nonemp A_bdd
#align antitone.map_Inf_of_continuous_at' Antitone.map_sInf_of_continuousAt'

/-- An antitone function continuous at the indexed infimum over a nonempty `Sort` sends this indexed
infimum to the indexed supremum of the composition. -/
theorem Antitone.map_iInf_of_continuousAt' {ι : Sort*} [Nonempty ι] {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iInf g)) (Af : Antitone f)
    (bdd : BddBelow (range g) := by bddDefault) : f (⨅ i, g i) = ⨆ i, f (g i) := by
  rw [iInf, Antitone.map_sInf_of_continuousAt' Cf Af (range_nonempty g) bdd, ← range_comp, iSup]
  rfl
#align antitone.map_infi_of_continuous_at' Antitone.map_iInf_of_continuousAt'

/-- An antitone function continuous at the supremum of a nonempty set sends this supremum to
the infimum of the image of this set. -/
theorem Antitone.map_sSup_of_continuousAt' {f : α → β} {A : Set α} (Cf : ContinuousAt f (sSup A))
    (Af : Antitone f) (A_nonemp : A.Nonempty) (A_bdd : BddAbove A := by bddDefault) :
    f (sSup A) = sInf (f '' A) :=
  Monotone.map_sSup_of_continuousAt' (β := βᵒᵈ) Cf Af.dual_right A_nonemp A_bdd
#align antitone.map_Sup_of_continuous_at' Antitone.map_sSup_of_continuousAt'

/-- An antitone function continuous at the indexed supremum over a nonempty `Sort` sends this
indexed supremum to the indexed infimum of the composition. -/
theorem Antitone.map_iSup_of_continuousAt' {ι : Sort*} [Nonempty ι] {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iSup g)) (Af : Antitone f)
    (bdd : BddAbove (range g) := by bddDefault) : f (⨆ i, g i) = ⨅ i, f (g i) := by
  rw [iSup, Antitone.map_sSup_of_continuousAt' Cf Af (range_nonempty g) bdd, ← range_comp, iInf]
  rfl
#align antitone.map_supr_of_continuous_at' Antitone.map_iSup_of_continuousAt'

end ConditionallyCompleteLinearOrder

section CompleteLinearOrder

variable [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β]
  [TopologicalSpace β] [OrderClosedTopology β] [Nonempty γ]

theorem sSup_mem_closure {α : Type u} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α]
    {s : Set α} (hs : s.Nonempty) : sSup s ∈ closure s :=
  (isLUB_sSup s).mem_closure hs
#align Sup_mem_closure sSup_mem_closure

theorem sInf_mem_closure {α : Type u} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α]
    {s : Set α} (hs : s.Nonempty) : sInf s ∈ closure s :=
  (isGLB_sInf s).mem_closure hs
#align Inf_mem_closure sInf_mem_closure

theorem IsClosed.sSup_mem {α : Type u} [TopologicalSpace α] [CompleteLinearOrder α]
    [OrderTopology α] {s : Set α} (hs : s.Nonempty) (hc : IsClosed s) : sSup s ∈ s :=
  (isLUB_sSup s).mem_of_isClosed hs hc
#align is_closed.Sup_mem IsClosed.sSup_mem

theorem IsClosed.sInf_mem {α : Type u} [TopologicalSpace α] [CompleteLinearOrder α]
    [OrderTopology α] {s : Set α} (hs : s.Nonempty) (hc : IsClosed s) : sInf s ∈ s :=
  (isGLB_sInf s).mem_of_isClosed hs hc
#align is_closed.Inf_mem IsClosed.sInf_mem

/-- A monotone function `f` sending `bot` to `bot` and continuous at the supremum of a set sends
this supremum to the supremum of the image of this set. -/
theorem Monotone.map_sSup_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s))
    (Mf : Monotone f) (fbot : f ⊥ = ⊥) : f (sSup s) = sSup (f '' s) := by
  cases' s.eq_empty_or_nonempty with h h
  · simp [h, fbot]
  · exact Mf.map_sSup_of_continuousAt' Cf h
#align monotone.map_Sup_of_continuous_at Monotone.map_sSup_of_continuousAt

/-- If a monotone function sending `bot` to `bot` is continuous at the indexed supremum over
a `Sort`, then it sends this indexed supremum to the indexed supremum of the composition. -/
theorem Monotone.map_iSup_of_continuousAt {ι : Sort*} {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iSup g)) (Mf : Monotone f) (fbot : f ⊥ = ⊥) :
    f (⨆ i, g i) = ⨆ i, f (g i) := by
  rw [iSup, Mf.map_sSup_of_continuousAt Cf fbot, ← range_comp, iSup]; rfl
#align monotone.map_supr_of_continuous_at Monotone.map_iSup_of_continuousAt

/-- A monotone function `f` sending `top` to `top` and continuous at the infimum of a set sends
this infimum to the infimum of the image of this set. -/
theorem Monotone.map_sInf_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s))
    (Mf : Monotone f) (ftop : f ⊤ = ⊤) : f (sInf s) = sInf (f '' s) :=
  Monotone.map_sSup_of_continuousAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual ftop
#align monotone.map_Inf_of_continuous_at Monotone.map_sInf_of_continuousAt

/-- If a monotone function sending `top` to `top` is continuous at the indexed infimum over
a `Sort`, then it sends this indexed infimum to the indexed infimum of the composition. -/
theorem Monotone.map_iInf_of_continuousAt {ι : Sort*} {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iInf g)) (Mf : Monotone f) (ftop : f ⊤ = ⊤) : f (iInf g) = iInf (f ∘ g) :=
  Monotone.map_iSup_of_continuousAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual ftop
#align monotone.map_infi_of_continuous_at Monotone.map_iInf_of_continuousAt

/-- An antitone function `f` sending `bot` to `top` and continuous at the supremum of a set sends
this supremum to the infimum of the image of this set. -/
theorem Antitone.map_sSup_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s))
    (Af : Antitone f) (fbot : f ⊥ = ⊤) : f (sSup s) = sInf (f '' s) :=
  Monotone.map_sSup_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (sSup s) from Cf) Af
    fbot
#align antitone.map_Sup_of_continuous_at Antitone.map_sSup_of_continuousAt

/-- An antitone function sending `bot` to `top` is continuous at the indexed supremum over
a `Sort`, then it sends this indexed supremum to the indexed supremum of the composition. -/
theorem Antitone.map_iSup_of_continuousAt {ι : Sort*} {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iSup g)) (Af : Antitone f) (fbot : f ⊥ = ⊤) :
    f (⨆ i, g i) = ⨅ i, f (g i) :=
  Monotone.map_iSup_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (iSup g) from Cf) Af
    fbot
#align antitone.map_supr_of_continuous_at Antitone.map_iSup_of_continuousAt

/-- An antitone function `f` sending `top` to `bot` and continuous at the infimum of a set sends
this infimum to the supremum of the image of this set. -/
theorem Antitone.map_sInf_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s))
    (Af : Antitone f) (ftop : f ⊤ = ⊥) : f (sInf s) = sSup (f '' s) :=
  Monotone.map_sInf_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (sInf s) from Cf) Af
    ftop
#align antitone.map_Inf_of_continuous_at Antitone.map_sInf_of_continuousAt

/-- If an antitone function sending `top` to `bot` is continuous at the indexed infimum over
a `Sort`, then it sends this indexed infimum to the indexed supremum of the composition. -/
theorem Antitone.map_iInf_of_continuousAt {ι : Sort*} {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iInf g)) (Af : Antitone f) (ftop : f ⊤ = ⊥) : f (iInf g) = iSup (f ∘ g) :=
  Monotone.map_iInf_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (iInf g) from Cf) Af
    ftop
#align antitone.map_infi_of_continuous_at Antitone.map_iInf_of_continuousAt

end CompleteLinearOrder

section ConditionallyCompleteLinearOrder

variable [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α]
  [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] [Nonempty γ]

theorem csSup_mem_closure {s : Set α} (hs : s.Nonempty) (B : BddAbove s) : sSup s ∈ closure s :=
  (isLUB_csSup hs B).mem_closure hs
#align cSup_mem_closure csSup_mem_closure

theorem csInf_mem_closure {s : Set α} (hs : s.Nonempty) (B : BddBelow s) : sInf s ∈ closure s :=
  (isGLB_csInf hs B).mem_closure hs
#align cInf_mem_closure csInf_mem_closure

theorem IsClosed.csSup_mem {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddAbove s) :
    sSup s ∈ s :=
  (isLUB_csSup hs B).mem_of_isClosed hs hc
#align is_closed.cSup_mem IsClosed.csSup_mem

theorem IsClosed.csInf_mem {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddBelow s) :
    sInf s ∈ s :=
  (isGLB_csInf hs B).mem_of_isClosed hs hc
#align is_closed.cInf_mem IsClosed.csInf_mem

theorem IsClosed.isLeast_csInf {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddBelow s) :
    IsLeast s (sInf s) :=
  ⟨hc.csInf_mem hs B, (isGLB_csInf hs B).1⟩

theorem IsClosed.isGreatest_csSup {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddAbove s) :
    IsGreatest s (sSup s) :=
  IsClosed.isLeast_csInf (α := αᵒᵈ) hc hs B

/-- If a monotone function is continuous at the supremum of a nonempty bounded above set `s`,
then it sends this supremum to the supremum of the image of `s`. -/
theorem Monotone.map_csSup_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s))
    (Mf : Monotone f) (ne : s.Nonempty) (H : BddAbove s) : f (sSup s) = sSup (f '' s) := by
  refine' ((isLUB_csSup (ne.image f) (Mf.map_bddAbove H)).unique _).symm
  refine' (isLUB_csSup ne H).isLUB_of_tendsto (fun x _ y _ xy => Mf xy) ne _
  exact Cf.mono_left inf_le_left
#align monotone.map_cSup_of_continuous_at Monotone.map_csSup_of_continuousAt

/-- If a monotone function is continuous at the indexed supremum of a bounded function on
a nonempty `Sort`, then it sends this supremum to the supremum of the composition. -/
theorem Monotone.map_ciSup_of_continuousAt {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨆ i, g i))
    (Mf : Monotone f) (H : BddAbove (range g)) : f (⨆ i, g i) = ⨆ i, f (g i) := by
  rw [iSup, Mf.map_csSup_of_continuousAt Cf (range_nonempty _) H, ← range_comp, iSup]; rfl
#align monotone.map_csupr_of_continuous_at Monotone.map_ciSup_of_continuousAt

/-- If a monotone function is continuous at the infimum of a nonempty bounded below set `s`,
then it sends this infimum to the infimum of the image of `s`. -/
theorem Monotone.map_csInf_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s))
    (Mf : Monotone f) (ne : s.Nonempty) (H : BddBelow s) : f (sInf s) = sInf (f '' s) :=
  Monotone.map_csSup_of_continuousAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual ne H
#align monotone.map_cInf_of_continuous_at Monotone.map_csInf_of_continuousAt

/-- A continuous monotone function sends indexed infimum to indexed infimum in conditionally
complete linear order, under a boundedness assumption. -/
theorem Monotone.map_ciInf_of_continuousAt {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨅ i, g i))
    (Mf : Monotone f) (H : BddBelow (range g)) : f (⨅ i, g i) = ⨅ i, f (g i) :=
  Monotone.map_ciSup_of_continuousAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual H
#align monotone.map_cinfi_of_continuous_at Monotone.map_ciInf_of_continuousAt

/-- If an antitone function is continuous at the supremum of a nonempty bounded above set `s`,
then it sends this supremum to the infimum of the image of `s`. -/
theorem Antitone.map_csSup_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s))
    (Af : Antitone f) (ne : s.Nonempty) (H : BddAbove s) : f (sSup s) = sInf (f '' s) :=
  Monotone.map_csSup_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (sSup s) from Cf) Af
    ne H
#align antitone.map_cSup_of_continuous_at Antitone.map_csSup_of_continuousAt

/-- If an antitone function is continuous at the indexed supremum of a bounded function on
a nonempty `Sort`, then it sends this supremum to the infimum of the composition. -/
theorem Antitone.map_ciSup_of_continuousAt {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨆ i, g i))
    (Af : Antitone f) (H : BddAbove (range g)) : f (⨆ i, g i) = ⨅ i, f (g i) :=
  Monotone.map_ciSup_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (⨆ i, g i) from Cf)
    Af H
#align antitone.map_csupr_of_continuous_at Antitone.map_ciSup_of_continuousAt

/-- If an antitone function is continuous at the infimum of a nonempty bounded below set `s`,
then it sends this infimum to the supremum of the image of `s`. -/
theorem Antitone.map_csInf_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s))
    (Af : Antitone f) (ne : s.Nonempty) (H : BddBelow s) : f (sInf s) = sSup (f '' s) :=
  Monotone.map_csInf_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (sInf s) from Cf) Af
    ne H
#align antitone.map_cInf_of_continuous_at Antitone.map_csInf_of_continuousAt

/-- A continuous antitone function sends indexed infimum to indexed supremum in conditionally
complete linear order, under a boundedness assumption. -/
theorem Antitone.map_ciInf_of_continuousAt {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨅ i, g i))
    (Af : Antitone f) (H : BddBelow (range g)) : f (⨅ i, g i) = ⨆ i, f (g i) :=
  Monotone.map_ciInf_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (⨅ i, g i) from Cf)
    Af H
#align antitone.map_cinfi_of_continuous_at Antitone.map_ciInf_of_continuousAt

/-- A monotone map has a limit to the left of any point `x`, equal to `sSup (f '' (Iio x))`. -/
theorem Monotone.tendsto_nhdsWithin_Iio {α β : Type*} [LinearOrder α] [TopologicalSpace α]
    [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β]
    {f : α → β} (Mf : Monotone f) (x : α) : Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x))) := by
  rcases eq_empty_or_nonempty (Iio x) with (h | h); · simp [h]
  refine' tendsto_order.2 ⟨fun l hl => _, fun m hm => _⟩
  · obtain ⟨z, zx, lz⟩ : ∃ a : α, a < x ∧ l < f a := by
      simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_lt_csSup (nonempty_image_iff.2 h) hl
    exact mem_of_superset (Ioo_mem_nhdsWithin_Iio' zx) fun y hy => lz.trans_le (Mf hy.1.le)
  · refine mem_of_superset self_mem_nhdsWithin fun _ hy => lt_of_le_of_lt ?_ hm
    exact le_csSup (Mf.map_bddAbove bddAbove_Iio) (mem_image_of_mem _ hy)
#align monotone.tendsto_nhds_within_Iio Monotone.tendsto_nhdsWithin_Iio

/-- A monotone map has a limit to the right of any point `x`, equal to `sInf (f '' (Ioi x))`. -/
theorem Monotone.tendsto_nhdsWithin_Ioi {α β : Type*} [LinearOrder α] [TopologicalSpace α]
    [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β]
    {f : α → β} (Mf : Monotone f) (x : α) : Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioi x))) :=
  Monotone.tendsto_nhdsWithin_Iio (α := αᵒᵈ) (β := βᵒᵈ) Mf.dual x
#align monotone.tendsto_nhds_within_Ioi Monotone.tendsto_nhdsWithin_Ioi

end ConditionallyCompleteLinearOrder

section NhdsWithPos

section LinearOrderedAddCommGroup

variable [LinearOrder α] [Zero α] [TopologicalSpace α] [OrderTopology α]

@[deprecated Ioo_mem_nhdsWithin_Ioi']
theorem eventually_nhdsWithin_pos_mem_Ioo {ε : α} (h : 0 < ε) : ∀ᶠ x in 𝓝[>] 0, x ∈ Ioo 0 ε :=
  Ioo_mem_nhdsWithin_Ioi' h
#align eventually_nhds_within_pos_mem_Ioo eventually_nhdsWithin_pos_mem_Ioo

@[deprecated Ioc_mem_nhdsWithin_Ioi']
theorem eventually_nhdsWithin_pos_mem_Ioc {ε : α} (h : 0 < ε) : ∀ᶠ x in 𝓝[>] 0, x ∈ Ioc 0 ε :=
  Ioc_mem_nhdsWithin_Ioi' h
#align eventually_nhds_within_pos_mem_Ioc eventually_nhdsWithin_pos_mem_Ioc

end LinearOrderedAddCommGroup

end NhdsWithPos

end OrderTopology
